:: AFF_3 semantic presentation
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_DES1 means :
E1:
:: AFF_3:def 1
for b
1, b
2, b
3 being
Subset of a
1for b
4, b
5, b
6, b
7, b
8, b
9, b
10, b
11, b
12 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 is
is_line & b
3 is
is_line & b
4 in b
1 & b
5 in b
1 & b
6 in b
1 & b
4 in b
2 & b
7 in b
2 & b
8 in b
2 & b
4 in b
3 & b
9 in b
3 & b
10 in b
3 &
LIN b
7,b
5,b
11 &
LIN b
8,b
6,b
11 &
LIN b
7,b
9,b
12 &
LIN b
8,b
10,b
12 & b
5,b
9 // b
6,b
10 ) implies ( not b
2 <> b
1 or not b
2 <> b
3 or not b
1 <> b
3 or not b
4 <> b
5 or not b
4 <> b
7 or not b
4 <> b
9 or not b
11 <> b
12 or
LIN b
7,b
5,b
9 or
LIN b
8,b
6,b
10 or not b
5 <> b
6 or b
5,b
9 // b
11,b
12 ) );
end;
:: deftheorem E1 defines satisfying_DES1 AFF_3:def 1 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_DES1 iff for b
2, b
3, b
4 being
Subset of b
1for b
5, b
6, b
7, b
8, b
9, b
10, b
11, b
12, b
13 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 is
is_line & b
4 is
is_line & b
5 in b
2 & b
6 in b
2 & b
7 in b
2 & b
5 in b
3 & b
8 in b
3 & b
9 in b
3 & b
5 in b
4 & b
10 in b
4 & b
11 in b
4 &
LIN b
8,b
6,b
12 &
LIN b
9,b
7,b
12 &
LIN b
8,b
10,b
13 &
LIN b
9,b
11,b
13 & b
6,b
10 // b
7,b
11 ) implies ( not b
3 <> b
2 or not b
3 <> b
4 or not b
2 <> b
4 or not b
5 <> b
6 or not b
5 <> b
8 or not b
5 <> b
10 or not b
12 <> b
13 or
LIN b
8,b
6,b
10 or
LIN b
9,b
7,b
11 or not b
6 <> b
7 or b
6,b
10 // b
12,b
13 ) ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_DES1_1 means :
E2:
:: AFF_3:def 2
for b
1, b
2, b
3 being
Subset of a
1for b
4, b
5, b
6, b
7, b
8, b
9, b
10, b
11, b
12 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 is
is_line & b
3 is
is_line & b
4 in b
1 & b
5 in b
1 & b
6 in b
1 & b
4 in b
2 & b
7 in b
2 & b
8 in b
2 & b
4 in b
3 & b
9 in b
3 & b
10 in b
3 &
LIN b
7,b
5,b
11 &
LIN b
8,b
6,b
11 &
LIN b
7,b
9,b
12 &
LIN b
8,b
10,b
12 & b
5,b
9 // b
11,b
12 ) implies ( not b
2 <> b
1 or not b
2 <> b
3 or not b
1 <> b
3 or not b
4 <> b
5 or not b
4 <> b
7 or not b
4 <> b
9 or not b
11 <> b
12 or not b
9 <> b
12 or
LIN b
7,b
5,b
9 or
LIN b
8,b
6,b
10 or b
5,b
9 // b
6,b
10 ) );
end;
:: deftheorem E2 defines satisfying_DES1_1 AFF_3:def 2 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_DES1_1 iff for b
2, b
3, b
4 being
Subset of b
1for b
5, b
6, b
7, b
8, b
9, b
10, b
11, b
12, b
13 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 is
is_line & b
4 is
is_line & b
5 in b
2 & b
6 in b
2 & b
7 in b
2 & b
5 in b
3 & b
8 in b
3 & b
9 in b
3 & b
5 in b
4 & b
10 in b
4 & b
11 in b
4 &
LIN b
8,b
6,b
12 &
LIN b
9,b
7,b
12 &
LIN b
8,b
10,b
13 &
LIN b
9,b
11,b
13 & b
6,b
10 // b
12,b
13 ) implies ( not b
3 <> b
2 or not b
3 <> b
4 or not b
2 <> b
4 or not b
5 <> b
6 or not b
5 <> b
8 or not b
5 <> b
10 or not b
12 <> b
13 or not b
10 <> b
13 or
LIN b
8,b
6,b
10 or
LIN b
9,b
7,b
11 or b
6,b
10 // b
7,b
11 ) ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_DES1_2 means :
E3:
:: AFF_3:def 3
for b
1, b
2, b
3 being
Subset of a
1for b
4, b
5, b
6, b
7, b
8, b
9, b
10, b
11, b
12 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 is
is_line & b
3 is
is_line & b
4 in b
1 & b
5 in b
1 & b
6 in b
1 & b
4 in b
2 & b
7 in b
2 & b
8 in b
2 & b
9 in b
3 & b
10 in b
3 &
LIN b
7,b
5,b
11 &
LIN b
8,b
6,b
11 &
LIN b
7,b
9,b
12 &
LIN b
8,b
10,b
12 & b
5,b
9 // b
6,b
10 & b
5,b
9 // b
11,b
12 ) implies ( not b
2 <> b
1 or not b
2 <> b
3 or not b
1 <> b
3 or not b
4 <> b
5 or not b
4 <> b
7 or not b
4 <> b
9 or not b
11 <> b
12 or
LIN b
7,b
5,b
9 or
LIN b
8,b
6,b
10 or not b
9 <> b
10 or b
4 in b
3 ) );
end;
:: deftheorem E3 defines satisfying_DES1_2 AFF_3:def 3 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_DES1_2 iff for b
2, b
3, b
4 being
Subset of b
1for b
5, b
6, b
7, b
8, b
9, b
10, b
11, b
12, b
13 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 is
is_line & b
4 is
is_line & b
5 in b
2 & b
6 in b
2 & b
7 in b
2 & b
5 in b
3 & b
8 in b
3 & b
9 in b
3 & b
10 in b
4 & b
11 in b
4 &
LIN b
8,b
6,b
12 &
LIN b
9,b
7,b
12 &
LIN b
8,b
10,b
13 &
LIN b
9,b
11,b
13 & b
6,b
10 // b
7,b
11 & b
6,b
10 // b
12,b
13 ) implies ( not b
3 <> b
2 or not b
3 <> b
4 or not b
2 <> b
4 or not b
5 <> b
6 or not b
5 <> b
8 or not b
5 <> b
10 or not b
12 <> b
13 or
LIN b
8,b
6,b
10 or
LIN b
9,b
7,b
11 or not b
10 <> b
11 or b
5 in b
4 ) ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_DES1_3 means :
E4:
:: AFF_3:def 4
for b
1, b
2, b
3 being
Subset of a
1for b
4, b
5, b
6, b
7, b
8, b
9, b
10, b
11, b
12 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 is
is_line & b
3 is
is_line & b
4 in b
1 & b
5 in b
1 & b
6 in b
1 & b
7 in b
2 & b
8 in b
2 & b
4 in b
3 & b
9 in b
3 & b
10 in b
3 &
LIN b
7,b
5,b
11 &
LIN b
8,b
6,b
11 &
LIN b
7,b
9,b
12 &
LIN b
8,b
10,b
12 & b
5,b
9 // b
6,b
10 & b
5,b
9 // b
11,b
12 ) implies ( not b
2 <> b
1 or not b
2 <> b
3 or not b
1 <> b
3 or not b
4 <> b
5 or not b
4 <> b
7 or not b
4 <> b
9 or not b
11 <> b
12 or
LIN b
7,b
5,b
9 or
LIN b
8,b
6,b
10 or not b
7 <> b
8 or not b
5 <> b
6 or b
4 in b
2 ) );
end;
:: deftheorem E4 defines satisfying_DES1_3 AFF_3:def 4 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_DES1_3 iff for b
2, b
3, b
4 being
Subset of b
1for b
5, b
6, b
7, b
8, b
9, b
10, b
11, b
12, b
13 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 is
is_line & b
4 is
is_line & b
5 in b
2 & b
6 in b
2 & b
7 in b
2 & b
8 in b
3 & b
9 in b
3 & b
5 in b
4 & b
10 in b
4 & b
11 in b
4 &
LIN b
8,b
6,b
12 &
LIN b
9,b
7,b
12 &
LIN b
8,b
10,b
13 &
LIN b
9,b
11,b
13 & b
6,b
10 // b
7,b
11 & b
6,b
10 // b
12,b
13 ) implies ( not b
3 <> b
2 or not b
3 <> b
4 or not b
2 <> b
4 or not b
5 <> b
6 or not b
5 <> b
8 or not b
5 <> b
10 or not b
12 <> b
13 or
LIN b
8,b
6,b
10 or
LIN b
9,b
7,b
11 or not b
8 <> b
9 or not b
6 <> b
7 or b
5 in b
3 ) ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_DES2 means :
E5:
:: AFF_3:def 5
for b
1, b
2, b
3 being
Subset of a
1for b
4, b
5, b
6, b
7, b
8, b
9, b
10, b
11 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 is
is_line & b
3 is
is_line & b
4 in b
1 & b
5 in b
1 & b
6 in b
2 & b
7 in b
2 & b
8 in b
3 & b
9 in b
3 & b
1 // b
2 & b
1 // b
3 &
LIN b
6,b
4,b
10 &
LIN b
7,b
5,b
10 &
LIN b
6,b
8,b
11 &
LIN b
7,b
9,b
11 & b
4,b
8 // b
5,b
9 ) implies ( not b
1 <> b
2 or not b
1 <> b
3 or not b
2 <> b
3 or
LIN b
6,b
4,b
8 or
LIN b
7,b
5,b
9 or not b
10 <> b
11 or not b
4 <> b
5 or b
4,b
8 // b
10,b
11 ) );
end;
:: deftheorem E5 defines satisfying_DES2 AFF_3:def 5 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_DES2 iff for b
2, b
3, b
4 being
Subset of b
1for b
5, b
6, b
7, b
8, b
9, b
10, b
11, b
12 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 is
is_line & b
4 is
is_line & b
5 in b
2 & b
6 in b
2 & b
7 in b
3 & b
8 in b
3 & b
9 in b
4 & b
10 in b
4 & b
2 // b
3 & b
2 // b
4 &
LIN b
7,b
5,b
11 &
LIN b
8,b
6,b
11 &
LIN b
7,b
9,b
12 &
LIN b
8,b
10,b
12 & b
5,b
9 // b
6,b
10 ) implies ( not b
2 <> b
3 or not b
2 <> b
4 or not b
3 <> b
4 or
LIN b
7,b
5,b
9 or
LIN b
8,b
6,b
10 or not b
11 <> b
12 or not b
5 <> b
6 or b
5,b
9 // b
11,b
12 ) ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_DES2_1 means :
E6:
:: AFF_3:def 6
for b
1, b
2, b
3 being
Subset of a
1for b
4, b
5, b
6, b
7, b
8, b
9, b
10, b
11 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 is
is_line & b
3 is
is_line & b
4 in b
1 & b
5 in b
1 & b
6 in b
2 & b
7 in b
2 & b
8 in b
3 & b
9 in b
3 & b
1 // b
2 & b
1 // b
3 &
LIN b
6,b
4,b
10 &
LIN b
7,b
5,b
10 &
LIN b
6,b
8,b
11 &
LIN b
7,b
9,b
11 & b
4,b
8 // b
10,b
11 ) implies ( not b
1 <> b
2 or not b
1 <> b
3 or not b
2 <> b
3 or
LIN b
6,b
4,b
8 or
LIN b
7,b
5,b
9 or not b
10 <> b
11 or b
4,b
8 // b
5,b
9 ) );
end;
:: deftheorem E6 defines satisfying_DES2_1 AFF_3:def 6 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_DES2_1 iff for b
2, b
3, b
4 being
Subset of b
1for b
5, b
6, b
7, b
8, b
9, b
10, b
11, b
12 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 is
is_line & b
4 is
is_line & b
5 in b
2 & b
6 in b
2 & b
7 in b
3 & b
8 in b
3 & b
9 in b
4 & b
10 in b
4 & b
2 // b
3 & b
2 // b
4 &
LIN b
7,b
5,b
11 &
LIN b
8,b
6,b
11 &
LIN b
7,b
9,b
12 &
LIN b
8,b
10,b
12 & b
5,b
9 // b
11,b
12 ) implies ( not b
2 <> b
3 or not b
2 <> b
4 or not b
3 <> b
4 or
LIN b
7,b
5,b
9 or
LIN b
8,b
6,b
10 or not b
11 <> b
12 or b
5,b
9 // b
6,b
10 ) ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_DES2_2 means :
E7:
:: AFF_3:def 7
for b
1, b
2, b
3 being
Subset of a
1for b
4, b
5, b
6, b
7, b
8, b
9, b
10, b
11 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 is
is_line & b
3 is
is_line & b
4 in b
1 & b
5 in b
1 & b
6 in b
2 & b
7 in b
2 & b
8 in b
3 & b
9 in b
3 & b
1 // b
3 &
LIN b
6,b
4,b
10 &
LIN b
7,b
5,b
10 &
LIN b
6,b
8,b
11 &
LIN b
7,b
9,b
11 & b
4,b
8 // b
5,b
9 & b
4,b
8 // b
10,b
11 ) implies ( not b
1 <> b
2 or not b
1 <> b
3 or not b
2 <> b
3 or
LIN b
6,b
4,b
8 or
LIN b
7,b
5,b
9 or not b
10 <> b
11 or not b
4 <> b
5 or b
1 // b
2 ) );
end;
:: deftheorem E7 defines satisfying_DES2_2 AFF_3:def 7 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_DES2_2 iff for b
2, b
3, b
4 being
Subset of b
1for b
5, b
6, b
7, b
8, b
9, b
10, b
11, b
12 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 is
is_line & b
4 is
is_line & b
5 in b
2 & b
6 in b
2 & b
7 in b
3 & b
8 in b
3 & b
9 in b
4 & b
10 in b
4 & b
2 // b
4 &
LIN b
7,b
5,b
11 &
LIN b
8,b
6,b
11 &
LIN b
7,b
9,b
12 &
LIN b
8,b
10,b
12 & b
5,b
9 // b
6,b
10 & b
5,b
9 // b
11,b
12 ) implies ( not b
2 <> b
3 or not b
2 <> b
4 or not b
3 <> b
4 or
LIN b
7,b
5,b
9 or
LIN b
8,b
6,b
10 or not b
11 <> b
12 or not b
5 <> b
6 or b
2 // b
3 ) ) );
definition
let c
1 be
AffinPlane;
attr a
1 is
satisfying_DES2_3 means :
E8:
:: AFF_3:def 8
for b
1, b
2, b
3 being
Subset of a
1for b
4, b
5, b
6, b
7, b
8, b
9, b
10, b
11 being
Element of a
1 holds
( ( b
1 is
is_line & b
2 is
is_line & b
3 is
is_line & b
4 in b
1 & b
5 in b
1 & b
6 in b
2 & b
7 in b
2 & b
8 in b
3 & b
9 in b
3 & b
1 // b
2 &
LIN b
6,b
4,b
10 &
LIN b
7,b
5,b
10 &
LIN b
6,b
8,b
11 &
LIN b
7,b
9,b
11 & b
4,b
8 // b
5,b
9 & b
4,b
8 // b
10,b
11 ) implies ( not b
1 <> b
2 or not b
1 <> b
3 or not b
2 <> b
3 or
LIN b
6,b
4,b
8 or
LIN b
7,b
5,b
9 or not b
10 <> b
11 or not b
8 <> b
9 or b
1 // b
3 ) );
end;
:: deftheorem E8 defines satisfying_DES2_3 AFF_3:def 8 :
for b
1 being
AffinPlane holds
( b
1 is
satisfying_DES2_3 iff for b
2, b
3, b
4 being
Subset of b
1for b
5, b
6, b
7, b
8, b
9, b
10, b
11, b
12 being
Element of b
1 holds
( ( b
2 is
is_line & b
3 is
is_line & b
4 is
is_line & b
5 in b
2 & b
6 in b
2 & b
7 in b
3 & b
8 in b
3 & b
9 in b
4 & b
10 in b
4 & b
2 // b
3 &
LIN b
7,b
5,b
11 &
LIN b
8,b
6,b
11 &
LIN b
7,b
9,b
12 &
LIN b
8,b
10,b
12 & b
5,b
9 // b
6,b
10 & b
5,b
9 // b
11,b
12 ) implies ( not b
2 <> b
3 or not b
2 <> b
4 or not b
3 <> b
4 or
LIN b
7,b
5,b
9 or
LIN b
8,b
6,b
10 or not b
11 <> b
12 or not b
9 <> b
10 or b
2 // b
4 ) ) );
theorem :: AFF_3:1
canceled;
theorem :: AFF_3:2
canceled;
theorem :: AFF_3:3
canceled;
theorem :: AFF_3:4
canceled;
theorem :: AFF_3:5
canceled;
theorem :: AFF_3:6
canceled;
theorem :: AFF_3:7
canceled;
theorem :: AFF_3:8
canceled;
theorem :: AFF_3:9
proof
let c
1 be
AffinPlane;
assume E9:
c
1 is
satisfies_DES1
;
let c
2 be
Subset of c
1;
:: uses AFF_3:def 2let c
3, c
4 be
Subset of c
1;
let c
5, c
6, c
7, c
8, c
9, c
10, c
11, c
12, c
13 be
Element of c
1;
assume that
E10:
( c
2 is
is_line & c
3 is
is_line & c
4 is
is_line )
and
E11:
( c
3 <> c
2 & c
3 <> c
4 & c
2 <> c
4 )
and
E12:
( c
5 in c
2 & c
6 in c
2 & c
7 in c
2 & c
5 in c
3 & c
8 in c
3 & c
9 in c
3 & c
5 in c
4 & c
10 in c
4 & c
11 in c
4 & c
5 <> c
6 & c
5 <> c
8 & c
5 <> c
10 & c
12 <> c
13 & c
10 <> c
13 & not
LIN c
8,c
6,c
10 & not
LIN c
9,c
7,c
11 )
and
E13:
(
LIN c
8,c
6,c
12 &
LIN c
9,c
7,c
12 &
LIN c
8,c
10,c
13 &
LIN c
9,c
11,c
13 & c
6,c
10 // c
12,c
13 )
;
set c
14 =
Line c
8,c
6;
set c
15 =
Line c
8,c
10;
( c
8 <> c
6 & c
8 <> c
10 & c
6 <> c
10 )
by E12, AFF_1:16;
then E14:
(
Line c
8,c
6 is
is_line &
Line c
8,c
10 is
is_line & c
8 in Line c
8,c
6 & c
6 in Line c
8,c
6 & c
8 in Line c
8,c
10 & c
10 in Line c
8,c
10 & c
12 in Line c
8,c
6 & c
13 in Line c
8,c
10 )
by E13, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
E15:
( c
7 <> c
9 & c
9 <> c
11 & c
7 <> c
11 )
by E12, AFF_1:16;
E16:
(
Line c
8,c
10 <> c
3 &
Line c
8,c
6 <> c
3 )
by E10, E11, E12, E14, AFF_1:30;
E17:
( c
8 <> c
5 & c
8 <> c
6 & c
8 <> c
10 )
by E12, AFF_1:16;
E18:
Line c
8,c
6 <> Line c
8,c
10
by E12, E14, AFF_1:33;
E19:
not
LIN c
5,c
6,c
10
c
12 <> c
8
by E12, E13, AFF_1:69;
then E20:
c
12 <> c
9
by E10, E12, E14, E16, AFF_1:30;
c
13 <> c
8
proof
assume E21:
c
13 = c
8
;
( not
LIN c
8,c
10,c
6 & c
10,c
6 // c
13,c
12 &
LIN c
8,c
10,c
13 &
LIN c
8,c
6,c
12 )
by E12, E13, AFF_1:13, AFF_1:15;
hence
not verum
by E12, E21, AFF_1:69;
end;
then E21:
c
13 <> c
9
by E10, E12, E14, E16, AFF_1:30;
E22:
not
LIN c
9,c
12,c
13
proof
assume
LIN c
9,c
12,c
13
;
then E23:
LIN c
12,c
13,c
9
by AFF_1:15;
set c
16 =
Line c
12,c
13;
E24:
(
Line c
12,c
13 is
is_line & c
12 in Line c
12,c
13 & c
13 in Line c
12,c
13 & c
9 in Line c
12,c
13 )
by E12, E23, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
(
LIN c
12,c
9,c
7 &
LIN c
13,c
9,c
11 )
by E13, AFF_1:15;
then
( c
7 in Line c
12,c
13 & c
11 in Line c
12,c
13 )
by E20, E21, E24, AFF_1:39;
hence
not verum
by E12, E24, AFF_1:33;
end;
E23:
c
6 <> c
12
by E12, E13, AFF_1:23;
(
LIN c
5,c
6,c
7 &
LIN c
9,c
12,c
7 &
LIN c
5,c
10,c
11 &
LIN c
9,c
13,c
11 )
by E10, E12, E13, AFF_1:15, AFF_1:33;
hence
c
6,c
10 // c
7,c
11
by E9, E10, E12, E13, E14, E15, E16, E17, E18, E19, E22, E23, E1;
end;
theorem :: AFF_3:10
proof
let c
1 be
AffinPlane;
assume E9:
c
1 is
satisfies_DES1_1
;
let c
2 be
Subset of c
1;
:: uses AFF_3:def 1let c
3, c
4 be
Subset of c
1;
let c
5, c
6, c
7, c
8, c
9, c
10, c
11, c
12, c
13 be
Element of c
1;
assume that
E10:
( c
2 is
is_line & c
3 is
is_line & c
4 is
is_line )
and
E11:
( c
3 <> c
2 & c
3 <> c
4 & c
2 <> c
4 )
and
E12:
( c
5 in c
2 & c
6 in c
2 & c
7 in c
2 & c
5 in c
3 & c
8 in c
3 & c
9 in c
3 & c
5 in c
4 & c
10 in c
4 & c
11 in c
4 & c
5 <> c
6 & c
5 <> c
8 & c
5 <> c
10 & c
12 <> c
13 & not
LIN c
8,c
6,c
10 & not
LIN c
9,c
7,c
11 & c
6 <> c
7 )
and
E13:
(
LIN c
8,c
6,c
12 &
LIN c
9,c
7,c
12 &
LIN c
8,c
10,c
13 &
LIN c
9,c
11,c
13 & c
6,c
10 // c
7,c
11 )
;
set c
14 =
Line c
8,c
6;
set c
15 =
Line c
8,c
10;
( c
8 <> c
6 & c
8 <> c
10 & c
6 <> c
10 )
by E12, AFF_1:16;
then E14:
(
Line c
8,c
6 is
is_line &
Line c
8,c
10 is
is_line & c
8 in Line c
8,c
6 & c
6 in Line c
8,c
6 & c
8 in Line c
8,c
10 & c
10 in Line c
8,c
10 & c
12 in Line c
8,c
6 & c
13 in Line c
8,c
10 )
by E13, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
E15:
( c
7 <> c
9 & c
9 <> c
11 & c
7 <> c
11 )
by E12, AFF_1:16;
E16:
Line c
8,c
6 <> c
3
by E10, E11, E12, E14, AFF_1:30;
E17:
Line c
8,c
10 <> c
3
by E10, E11, E12, E14, AFF_1:30;
E18:
(
Line c
8,c
10 <> c
3 &
Line c
8,c
6 <> c
3 )
by E10, E11, E12, E14, AFF_1:30;
E19:
( c
8 <> c
5 & c
8 <> c
6 & c
8 <> c
10 )
by E12, AFF_1:16;
E20:
Line c
8,c
6 <> Line c
8,c
10
by E12, E14, AFF_1:33;
E21:
not
LIN c
5,c
6,c
10
E22:
c
10 <> c
11
proof
assume
c
10 = c
11
;
then
( c
10,c
6 // c
10,c
7 &
LIN c
5,c
6,c
7 & not
LIN c
5,c
10,c
6 )
by E10, E12, E13, E21, AFF_1:13, AFF_1:15, AFF_1:33;
hence
not verum
by E12, AFF_1:23;
end;
E23:
now
assume E24:
not
LIN c
9,c
12,c
13
;
(
LIN c
5,c
6,c
7 &
LIN c
9,c
12,c
7 &
LIN c
5,c
10,c
11 &
LIN c
9,c
13,c
11 )
by E10, E12, E13, AFF_1:15, AFF_1:33;
hence
c
6,c
10 // c
12,c
13
by E9, E10, E12, E13, E14, E15, E18, E19, E20, E21, E22, E24, E2;
end;
now
assume E24:
LIN c
9,c
12,c
13
;
set c
16 =
Line c
9,c
7;
set c
17 =
Line c
9,c
11;
E25:
LIN c
9,c
13,c
12
by E24, AFF_1:15;
E26:
(
Line c
9,c
7 is
is_line &
Line c
9,c
11 is
is_line & c
9 in Line c
9,c
7 & c
7 in Line c
9,c
7 & c
12 in Line c
9,c
7 & c
9 in Line c
9,c
11 & c
11 in Line c
9,c
11 & c
13 in Line c
9,c
11 )
by E13, E15, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
then E27:
Line c
9,c
7 <> Line c
9,c
11
by E12, AFF_1:33;
E28:
now
assume
c
9 <> c
12
;
then E29:
c
13 in Line c
9,c
7
by E24, E26, AFF_1:39;
then E30:
c
13 = c
9
by E26, E27, AFF_1:30;
LIN c
8,c
10,c
9
by E13, E26, E27, E29, AFF_1:30;
then
c
9 in Line c
8,c
10
by AFF_1:def 2;
then E31:
c
8 = c
9
by E10, E12, E14, E17, AFF_1:30;
Line c
9,c
7 <> Line c
8,c
6
proof
assume
Line c
9,c
7 = Line c
8,c
6
;
then
LIN c
6,c
7,c
8
by E14, E26, AFF_1:33;
then
c
8 in c
2
by E10, E12, AFF_1:39;
hence
not verum
by E10, E11, E12, AFF_1:30;
end;
then
c
12 = c
13
by E14, E26, E30, E31, AFF_1:30;
hence
c
6,c
10 // c
12,c
13
by AFF_1:12;
end;
now
assume
c
9 <> c
13
;
then E29:
c
12 in Line c
9,c
11
by E25, E26, AFF_1:39;
then E30:
c
12 = c
9
by E26, E27, AFF_1:30;
LIN c
8,c
6,c
9
by E13, E26, E27, E29, AFF_1:30;
then
c
9 in Line c
8,c
6
by AFF_1:def 2;
then E31:
c
8 = c
9
by E10, E12, E14, E16, AFF_1:30;
Line c
9,c
11 <> Line c
8,c
10
proof
assume
Line c
9,c
11 = Line c
8,c
10
;
then
LIN c
10,c
11,c
8
by E14, E26, AFF_1:33;
then
c
8 in c
4
by E10, E12, E22, AFF_1:39;
hence
not verum
by E10, E11, E12, AFF_1:30;
end;
then
c
12 = c
13
by E14, E26, E30, E31, AFF_1:30;
hence
c
6,c
10 // c
12,c
13
by AFF_1:12;
end;
hence
c
6,c
10 // c
12,c
13
by E12, E28;
end;
hence
c
6,c
10 // c
12,c
13
by E23;
end;
theorem :: AFF_3:11
proof
let c
1 be
AffinPlane;
assume E9:
c
1 is
satisfies_DES
;
let c
2 be
Subset of c
1;
:: uses AFF_3:def 1let c
3, c
4 be
Subset of c
1;
let c
5, c
6, c
7, c
8, c
9, c
10, c
11, c
12, c
13 be
Element of c
1;
assume that
E10:
( c
2 is
is_line & c
3 is
is_line & c
4 is
is_line )
and
E11:
( c
3 <> c
2 & c
3 <> c
4 & c
2 <> c
4 )
and
E12:
( c
5 in c
2 & c
6 in c
2 & c
7 in c
2 & c
5 in c
3 & c
8 in c
3 & c
9 in c
3 & c
5 in c
4 & c
10 in c
4 & c
11 in c
4 & c
5 <> c
6 & c
5 <> c
8 & c
5 <> c
10 & c
12 <> c
13 & not
LIN c
8,c
6,c
10 & not
LIN c
9,c
7,c
11 & c
6 <> c
7 )
and
E13:
(
LIN c
8,c
6,c
12 &
LIN c
9,c
7,c
12 &
LIN c
8,c
10,c
13 &
LIN c
9,c
11,c
13 & c
6,c
10 // c
7,c
11 )
;
set c
14 =
Line c
9,c
7;
set c
15 =
Line c
9,c
11;
E14:
( c
6 <> c
8 & c
6 <> c
10 & c
8 <> c
10 & c
7 <> c
9 & c
7 <> c
11 & c
9 <> c
11 )
by E12, AFF_1:16;
then E15:
(
Line c
9,c
7 is
is_line &
Line c
9,c
11 is
is_line & c
9 in Line c
9,c
7 & c
7 in Line c
9,c
7 & c
12 in Line c
9,c
7 & c
9 in Line c
9,c
11 & c
11 in Line c
9,c
11 & c
13 in Line c
9,c
11 )
by E13, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
E16:
not
LIN c
5,c
6,c
10
E17:
c
5 <> c
7
proof
assume E18:
c
5 = c
7
;
(
LIN c
5,c
6,c
7 &
LIN c
5,c
10,c
11 )
by E10, E12, AFF_1:33;
hence
not verum
by E13, E14, E16, E18, AFF_1:69;
end;
E18:
c
5 <> c
11
proof
assume E19:
c
5 = c
11
;
(
LIN c
5,c
6,c
7 &
LIN c
5,c
10,c
11 & c
10,c
6 // c
11,c
7 & not
LIN c
5,c
10,c
6 )
by E10, E12, E13, E16, AFF_1:13, AFF_1:15, AFF_1:33;
hence
not verum
by E17, E19, AFF_1:69;
end;
E19:
c
10 <> c
11
proof
assume
c
10 = c
11
;
then
(
LIN c
5,c
6,c
7 & c
10,c
6 // c
10,c
7 & not
LIN c
5,c
10,c
6 )
by E10, E12, E13, E16, AFF_1:13, AFF_1:15, AFF_1:33;
hence
not verum
by E12, AFF_1:23;
end;
E20:
(
Line c
9,c
7 <> c
3 &
Line c
9,c
11 <> c
3 &
Line c
9,c
7 <> Line c
9,c
11 )
by E10, E11, E12, E15, E17, E18, AFF_1:30, AFF_1:33;
set c
16 =
Line c
8,c
10;
E21:
(
Line c
8,c
10 is
is_line & c
8 in Line c
8,c
10 & c
10 in Line c
8,c
10 & c
13 in Line c
8,c
10 )
by E13, E14, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
then consider c
17 being
Subset of c
1 such that
E22:
( c
11 in c
17 &
Line c
8,c
10 // c
17 )
by AFF_1:63;
E23:
( c
17 is
is_line & c
17 // Line c
8,c
10 )
by E22, AFF_1:50;
not c
17 // c
3
then consider c
18 being
Element of c
1 such that
E24:
( c
18 in c
17 & c
18 in c
3 )
by E10, E23, AFF_1:72;
E25:
c
18 <> c
9
proof
assume
c
18 = c
9
;
then
Line c
9,c
11 = c
17
by E14, E15, E22, E23, E24, AFF_1:30;
then
Line c
8,c
10 = Line c
9,c
11
by E15, E21, E22, AFF_1:59;
then
LIN c
10,c
11,c
8
by E15, E21, AFF_1:33;
then
c
8 in c
4
by E10, E12, E19, AFF_1:39;
hence
not verum
by E10, E11, E12, AFF_1:30;
end;
( c
10,c
8 // c
11,c
18 & c
10,c
6 // c
11,c
7 )
by E13, E21, E22, E24, AFF_1:13, AFF_1:53;
then E26:
c
8,c
6 // c
18,c
7
by E9, E10, E11, E12, E24, AFF_2:def 4;
c
8,c
6 // c
8,c
12
by E13, AFF_1:def 1;
then
( c
18,c
7 // c
8,c
12 & c
8,c
13 // c
18,c
11 )
by E14, E21, E22, E24, E26, AFF_1:14, AFF_1:53;
then
( c
18,c
7 // c
8,c
12 & c
18,c
11 // c
8,c
13 )
by AFF_1:13;
then
c
7,c
11 // c
12,c
13
by E9, E10, E12, E14, E15, E20, E24, E25, AFF_2:def 4;
hence
c
6,c
10 // c
12,c
13
by E13, E14, AFF_1:14;
end;
theorem :: AFF_3:12
proof
let c
1 be
AffinPlane;
assume E9:
c
1 is
satisfies_DES
;
then E10:
c
1 is
satisfies_DES_1
by AFF_2:16;
let c
2 be
Subset of c
1;
:: uses AFF_3:def 3let c
3, c
4 be
Subset of c
1;
let c
5, c
6, c
7, c
8, c
9, c
10, c
11, c
12, c
13 be
Element of c
1;
assume that
E11:
( c
2 is
is_line & c
3 is
is_line & c
4 is
is_line )
and
E12:
( c
3 <> c
2 & c
3 <> c
4 & c
2 <> c
4 )
and
E13:
( c
5 in c
2 & c
6 in c
2 & c
7 in c
2 & c
5 in c
3 & c
8 in c
3 & c
9 in c
3 & c
10 in c
4 & c
11 in c
4 & c
5 <> c
6 & c
5 <> c
8 & c
5 <> c
10 & c
12 <> c
13 & not
LIN c
8,c
6,c
10 & not
LIN c
9,c
7,c
11 & c
10 <> c
11 )
and
E14:
(
LIN c
8,c
6,c
12 &
LIN c
9,c
7,c
12 &
LIN c
8,c
10,c
13 &
LIN c
9,c
11,c
13 & c
6,c
10 // c
7,c
11 & c
6,c
10 // c
12,c
13 )
;
E15:
( c
6 <> c
8 & c
6 <> c
10 & c
8 <> c
10 & c
7 <> c
9 & c
7 <> c
11 & c
9 <> c
11 )
by E13, AFF_1:16;
E16:
( c
9 <> c
7 & c
9 <> c
11 )
by E13, AFF_1:16;
set c
14 =
Line c
9,c
7;
set c
15 =
Line c
9,c
11;
E17:
(
Line c
9,c
7 is
is_line &
Line c
9,c
11 is
is_line & c
9 in Line c
9,c
7 & c
7 in Line c
9,c
7 & c
12 in Line c
9,c
7 & c
9 in Line c
9,c
11 & c
11 in Line c
9,c
11 & c
13 in Line c
9,c
11 )
by E14, E15, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
then E18:
Line c
9,c
7 <> Line c
9,c
11
by E13, AFF_1:33;
E19:
c
8 <> c
13
proof
assume E20:
c
8 = c
13
;
( not
LIN c
8,c
10,c
6 & c
10,c
6 // c
13,c
12 )
by E13, E14, AFF_1:13, AFF_1:15;
hence
not verum
by E13, E14, E20, AFF_1:69;
end;
E20:
c
9 <> c
13
proof
assume E21:
c
9 = c
13
;
c
7,c
11 // c
12,c
13
by E14, E15, AFF_1:14;
then
( c
11,c
7 // c
13,c
12 & not
LIN c
9,c
11,c
7 )
by E13, AFF_1:13, AFF_1:15;
hence
not verum
by E13, E14, E21, AFF_1:69;
end;
E21:
c
9 <> c
12
E22:
c
8 <> c
12
by E13, E14, AFF_1:69;
now
E23:
now
assume E24:
Line c
9,c
11 = c
3
;
LIN c
8,c
13,c
10
by E14, AFF_1:15;
then
c
10 in c
3
by E13, E17, E19, E24, AFF_1:39;
then
c
3 = Line c
10,c
11
by E13, E17, E24, AFF_1:71;
hence
c
5 in c
4
by E11, E13, AFF_1:71;
end;
now
assume E24:
Line c
9,c
11 <> c
3
;
set c
16 =
Line c
8,c
10;
E25:
(
Line c
8,c
10 is
is_line & c
8 in Line c
8,c
10 & c
10 in Line c
8,c
10 & c
13 in Line c
8,c
10 )
by E14, E15, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
then consider c
17 being
Subset of c
1 such that
E26:
( c
11 in c
17 &
Line c
8,c
10 // c
17 )
by AFF_1:63;
E27:
c
17 is
is_line
by E26, AFF_1:50;
not c
17 // c
3
then consider c
18 being
Element of c
1 such that
E28:
( c
18 in c
17 & c
18 in c
3 )
by E11, E27, AFF_1:72;
E29:
( c
13,c
8 // c
11,c
18 & c
8,c
10 // c
18,c
11 )
by E25, E26, E28, AFF_1:53;
then E30:
( c
11,c
18 // c
13,c
8 & c
8,c
10 // c
18,c
11 )
by AFF_1:13;
E31:
c
18 <> c
9
proof
assume
c
18 = c
9
;
then
Line c
9,c
11 = c
17
by E15, E17, E26, E27, E28, AFF_1:30;
then
Line c
8,c
10 = Line c
9,c
11
by E17, E25, E26, AFF_1:59;
then
(
LIN c
10,c
11,c
8 &
LIN c
10,c
11,c
9 )
by E17, E25, AFF_1:33;
then E32:
( c
8 in c
4 & c
9 in c
4 )
by E11, E13, AFF_1:39;
set c
19 =
Line c
8,c
6;
set c
20 =
Line c
6,c
10;
E33:
(
Line c
8,c
6 is
is_line & c
8 in Line c
8,c
6 & c
6 in Line c
8,c
6 & c
12 in Line c
8,c
6 )
by E14, E15, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
E34:
(
Line c
6,c
10 is
is_line & c
6 in Line c
6,c
10 & c
10 in Line c
6,c
10 )
by E15, AFF_1:26, AFF_1:def 3;
E35:
c
6 <> c
7
proof
assume
c
6 = c
7
;
then
LIN c
6,c
10,c
11
by E14, AFF_1:def 1;
then
c
11 in Line c
6,c
10
by AFF_1:def 2;
then
Line c
6,c
10 = c
4
by E11, E13, E34, AFF_1:30;
hence
not verum
by E13, E32, E34, AFF_1:33;
end;
c
8 <> c
9
proof
assume E36:
c
8 = c
9
;
Line c
9,c
7 <> Line c
8,c
6
proof
assume
Line c
9,c
7 = Line c
8,c
6
;
then
Line c
8,c
6 = c
2
by E11, E13, E17, E33, E35, AFF_1:30;
hence
not verum
by E11, E12, E13, E33, AFF_1:30;
end;
hence
not verum
by E17, E21, E33, E36, AFF_1:30;
end;
hence
not verum
by E11, E12, E13, E32, AFF_1:30;
end;
c
12,c
13 // c
7,c
11
by E14, E15, AFF_1:14;
then
c
11,c
7 // c
13,c
12
by AFF_1:13;
then E32:
c
18,c
7 // c
8,c
12
by E9, E11, E13, E16, E17, E18, E24, E28, E30, E31, AFF_2:def 4;
c
8,c
6 // c
8,c
12
by E14, AFF_1:def 1;
then
c
8,c
6 // c
18,c
7
by E22, E32, AFF_1:14;
hence
c
5 in c
4
by E10, E11, E12, E13, E14, E28, E29, AFF_2:def 5;
end;
hence
c
5 in c
4
by E23;
end;
hence
c
5 in c
4
;
end;
theorem :: AFF_3:13
proof
let c
1 be
AffinPlane;
assume E9:
c
1 is
satisfies_DES1_2
;
let c
2 be
Subset of c
1;
:: uses AFF_3:def 4let c
3, c
4 be
Subset of c
1;
let c
5, c
6, c
7, c
8, c
9, c
10, c
11, c
12, c
13 be
Element of c
1;
assume that
E10:
( c
2 is
is_line & c
3 is
is_line & c
4 is
is_line )
and
E11:
( c
3 <> c
2 & c
3 <> c
4 & c
2 <> c
4 )
and
E12:
( c
5 in c
2 & c
6 in c
2 & c
7 in c
2 & c
8 in c
3 & c
9 in c
3 & c
5 in c
4 & c
10 in c
4 & c
11 in c
4 & c
5 <> c
6 & c
5 <> c
8 & c
5 <> c
10 & c
12 <> c
13 & not
LIN c
8,c
6,c
10 & not
LIN c
9,c
7,c
11 & c
8 <> c
9 & c
6 <> c
7 )
and
E13:
(
LIN c
8,c
6,c
12 &
LIN c
9,c
7,c
12 &
LIN c
8,c
10,c
13 &
LIN c
9,c
11,c
13 & c
6,c
10 // c
7,c
11 & c
6,c
10 // c
12,c
13 )
;
assume E14:
not c
5 in c
3
;
E15:
( c
6 <> c
8 & c
6 <> c
10 & c
8 <> c
10 & c
7 <> c
9 & c
7 <> c
11 & c
9 <> c
11 )
by E12, AFF_1:16;
E16:
not
LIN c
5,c
10,c
6
E17:
c
10 <> c
11
proof
assume
c
10 = c
11
;
then
(
LIN c
5,c
6,c
7 & c
10,c
6 // c
10,c
7 )
by E10, E12, E13, AFF_1:13, AFF_1:33;
hence
not verum
by E12, E16, AFF_1:23;
end;
E18:
c
7,c
11 // c
12,c
13
by E13, E15, AFF_1:14;
E19:
( c
12 <> c
8 & c
12 <> c
9 & c
13 <> c
8 & c
13 <> c
9 )
proof
assume E20:
not ( c
12 <> c
8 & c
12 <> c
9 & c
13 <> c
8 & c
13 <> c
9 )
;
E21:
now
assume E22:
c
8 = c
13
;
( not
LIN c
8,c
10,c
6 & c
10,c
6 // c
13,c
12 )
by E12, E13, AFF_1:13, AFF_1:15;
hence
not verum
by E12, E13, E22, AFF_1:69;
end;
now
assume E22:
c
9 = c
13
;
( not
LIN c
9,c
11,c
7 & c
11,c
7 // c
13,c
12 )
by E12, E18, AFF_1:13, AFF_1:15;
hence
not verum
by E12, E13, E22, AFF_1:69;
end;
hence
not verum
by E12, E13, E18, E20, E21, AFF_1:69;
end;
E20:
not ( c
3 // c
2 & c
4 // c
3 )
set c
14 =
Line c
8,c
10;
set c
15 =
Line c
8,c
6;
set c
16 =
Line c
12,c
13;
set c
17 =
Line c
7,c
11;
set c
18 =
Line c
9,c
7;
E21:
(
Line c
8,c
10 is
is_line &
Line c
8,c
6 is
is_line &
Line c
12,c
13 is
is_line &
Line c
7,c
11 is
is_line &
Line c
9,c
7 is
is_line & c
12 in Line c
12,c
13 & c
13 in Line c
12,c
13 & c
8 in Line c
8,c
10 & c
10 in Line c
8,c
10 & c
8 in Line c
8,c
6 & c
6 in Line c
8,c
6 & c
7 in Line c
7,c
11 & c
11 in Line c
7,c
11 & c
9 in Line c
9,c
7 & c
7 in Line c
9,c
7 )
by E12, E15, AFF_1:38;
then E22:
( c
13 in Line c
8,c
10 & c
12 in Line c
8,c
6 & c
12 in Line c
9,c
7 )
by E13, E15, AFF_1:39;
E23:
now
assume
not c
3 // c
2
;
then consider c
19 being
Element of c
1 such that
E24:
( c
19 in c
3 & c
19 in c
2 )
by E10, AFF_1:72;
E25:
c
19 <> c
6
proof
assume E26:
c
19 = c
6
;
then E27:
( c
12 in c
3 & c
6 in c
3 )
by E10, E12, E13, E15, E24, AFF_1:39;
Line c
9,c
7 <> c
3
by E10, E11, E12, E21, E24, E26, AFF_1:30;
hence
not verum
by E10, E12, E19, E21, E22, E27, AFF_1:30;
end;
c
19 <> c
8
proof
assume E26:
c
19 = c
8
;
then
(
LIN c
8,c
6,c
7 &
LIN c
8,c
6,c
6 )
by E10, E12, E24, AFF_1:33;
then
LIN c
6,c
7,c
12
by E13, E15, AFF_1:17;
then
c
12 in c
2
by E10, E12, AFF_1:39;
then
( c
7,c
11 // c
7,c
13 or c
9 in c
2 )
by E10, E12, E18, E21, E22, AFF_1:30;
then
LIN c
7,c
11,c
13
by E10, E11, E12, E24, E26, AFF_1:30, AFF_1:def 1;
then
(
LIN c
13,c
11,c
7 &
LIN c
13,c
11,c
9 &
LIN c
13,c
11,c
11 )
by E13, AFF_1:15, AFF_1:16;
then
c
13 = c
11
by E12, AFF_1:17;
then
LIN c
10,c
11,c
8
by E13, AFF_1:15;
then
c
8 in c
4
by E10, E12, E17, AFF_1:39;
hence
not verum
by E10, E11, E12, E24, E26, AFF_1:30;
end;
then
c
19 in c
4
by E9, E10, E11, E12, E13, E17, E24, E25, E3;
hence
not verum
by E10, E11, E12, E14, E24, AFF_1:30;
end;
now
assume
not c
4 // c
3
;
then consider c
19 being
Element of c
1 such that
E24:
( c
19 in c
4 & c
19 in c
3 )
by E10, AFF_1:72;
E25:
c
19 <> c
10
proof
assume E26:
c
19 = c
10
;
then
(
LIN c
8,c
10,c
9 &
LIN c
8,c
10,c
10 )
by E10, E12, E24, AFF_1:33;
then
(
LIN c
13,c
9,c
10 &
LIN c
13,c
9,c
11 &
LIN c
13,c
9,c
9 )
by E13, E15, AFF_1:15, AFF_1:17;
then
LIN c
10,c
11,c
9
by E19, AFF_1:17;
then E27:
c
9 in c
4
by E10, E12, E17, AFF_1:39;
then E28:
c
10 = c
9
by E10, E11, E12, E24, E26, AFF_1:30;
LIN c
10,c
11,c
13
by E10, E11, E12, E13, E24, E26, E27, AFF_1:30;
then
c
13 in c
4
by E10, E12, E17, AFF_1:39;
then
c
4 = Line c
8,c
10
by E10, E12, E19, E21, E22, E28, AFF_1:30;
hence
not verum
by E10, E11, E12, E21, E27, AFF_1:30;
end;
E26:
c
19 <> c
8
proof
assume E27:
c
19 = c
8
;
then
(
LIN c
8,c
10,c
11 &
LIN c
8,c
10,c
10 )
by E10, E12, E24, AFF_1:33;
then
LIN c
10,c
11,c
13
by E13, E15, AFF_1:17;
then
( c
13 in c
4 &
LIN c
13,c
11,c
9 )
by E10, E12, E13, E17, AFF_1:15, AFF_1:39;
then
( c
13 = c
11 or c
9 in c
4 )
by E10, E12, AFF_1:39;
then
c
11,c
7 // c
11,c
12
by E10, E11, E12, E18, E24, E27, AFF_1:13, AFF_1:30;
then
LIN c
11,c
7,c
12
by AFF_1:def 1;
then
(
LIN c
12,c
7,c
11 &
LIN c
12,c
7,c
9 &
LIN c
12,c
7,c
7 )
by E13, AFF_1:15, AFF_1:16;
then
c
12 = c
7
by E12, AFF_1:17;
then
LIN c
6,c
7,c
8
by E13, AFF_1:15;
then
c
8 in c
2
by E10, E12, AFF_1:39;
hence
not verum
by E10, E11, E12, E24, E27, AFF_1:30;
end;
E27:
( not
LIN c
8,c
10,c
6 & not
LIN c
9,c
11,c
7 )
by E12, AFF_1:15;
( c
10,c
6 // c
13,c
12 & c
10,c
6 // c
11,c
7 )
by E13, AFF_1:13;
then
c
19 in c
2
by E9, E10, E11, E12, E13, E24, E25, E26, E27, E3;
hence
not verum
by E10, E11, E12, E14, E24, AFF_1:30;
end;
hence
not verum
by E20, E23;
end;
theorem :: AFF_3:14