:: AFF_3 semantic presentation
begin
definition
let AP be AffinPlane;
attrAP is satisfying_DES1 means :Def1: :: AFF_3:def 1
for A, P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q;
end;
:: deftheorem Def1 defines satisfying_DES1 AFF_3:def_1_:_
for AP being AffinPlane holds
( AP is satisfying_DES1 iff for A, P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q );
definition
let AP be AffinPlane;
attrAP is satisfying_DES1_1 means :Def2: :: AFF_3:def 2
for A, P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9;
end;
:: deftheorem Def2 defines satisfying_DES1_1 AFF_3:def_2_:_
for AP being AffinPlane holds
( AP is satisfying_DES1_1 iff for A, P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9 );
definition
let AP be AffinPlane;
attrAP is satisfying_DES1_2 means :Def3: :: AFF_3:def 3
for A, P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
o in C;
end;
:: deftheorem Def3 defines satisfying_DES1_2 AFF_3:def_3_:_
for AP being AffinPlane holds
( AP is satisfying_DES1_2 iff for A, P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
o in C );
definition
let AP be AffinPlane;
attrAP is satisfying_DES1_3 means :Def4: :: AFF_3:def 4
for A, P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & b <> b9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
o in P;
end;
:: deftheorem Def4 defines satisfying_DES1_3 AFF_3:def_4_:_
for AP being AffinPlane holds
( AP is satisfying_DES1_3 iff for A, P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & b <> b9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
o in P );
definition
let AP be AffinPlane;
attrAP is satisfying_DES2 means :Def5: :: AFF_3:def 5
for A, P, C being Subset of AP
for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q;
end;
:: deftheorem Def5 defines satisfying_DES2 AFF_3:def_5_:_
for AP being AffinPlane holds
( AP is satisfying_DES2 iff for A, P, C being Subset of AP
for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q );
definition
let AP be AffinPlane;
attrAP is satisfying_DES2_1 means :Def6: :: AFF_3:def 6
for A, P, C being Subset of AP
for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9;
end;
:: deftheorem Def6 defines satisfying_DES2_1 AFF_3:def_6_:_
for AP being AffinPlane holds
( AP is satisfying_DES2_1 iff for A, P, C being Subset of AP
for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9 );
definition
let AP be AffinPlane;
attrAP is satisfying_DES2_2 means :Def7: :: AFF_3:def 7
for A, P, C being Subset of AP
for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
A // P;
end;
:: deftheorem Def7 defines satisfying_DES2_2 AFF_3:def_7_:_
for AP being AffinPlane holds
( AP is satisfying_DES2_2 iff for A, P, C being Subset of AP
for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
A // P );
definition
let AP be AffinPlane;
attrAP is satisfying_DES2_3 means :Def8: :: AFF_3:def 8
for A, P, C being Subset of AP
for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
A // C;
end;
:: deftheorem Def8 defines satisfying_DES2_3 AFF_3:def_8_:_
for AP being AffinPlane holds
( AP is satisfying_DES2_3 iff for A, P, C being Subset of AP
for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
A // C );
theorem :: AFF_3:1
for AP being AffinPlane st AP is satisfying_DES1 holds
AP is satisfying_DES1_1
proof
let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES1 implies AP is satisfying_DES1_1 )
assume A1: AP is satisfying_DES1 ; ::_thesis: AP is satisfying_DES1_1
let A be Subset of AP; :: according to AFF_3:def_2 ::_thesis: for P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9
let P, C be Subset of AP; ::_thesis: for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9
let o, a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q implies a,c // a9,c9 )
assume that
A2: A is being_line and
A3: P is being_line and
A4: C is being_line and
A5: P <> A and
A6: P <> C and
A7: A <> C and
A8: o in A and
A9: a in A and
A10: a9 in A and
A11: o in P and
A12: ( b in P & b9 in P ) and
A13: ( o in C & c in C ) and
A14: c9 in C and
A15: o <> a and
A16: o <> b and
A17: o <> c and
A18: p <> q and
A19: c <> q and
A20: not LIN b,a,c and
A21: not LIN b9,a9,c9 and
A22: LIN b,a,p and
A23: LIN b9,a9,p and
A24: LIN b,c,q and
A25: LIN b9,c9,q and
A26: a,c // p,q ; ::_thesis: a,c // a9,c9
A27: ( LIN o,a,a9 & LIN b9,p,a9 ) by A2, A8, A9, A10, A23, AFF_1:6, AFF_1:21;
set K = Line (b,a);
A28: a in Line (b,a) by AFF_1:15;
then A29: Line (b,a) <> P by A2, A3, A5, A8, A9, A11, A15, AFF_1:18;
A30: not LIN o,a,c
proof
assume LIN o,a,c ; ::_thesis: contradiction
then c in A by A2, A8, A9, A15, AFF_1:25;
hence contradiction by A2, A4, A7, A8, A13, A17, AFF_1:18; ::_thesis: verum
end;
A31: p in Line (b,a) by A22, AFF_1:def_2;
A32: ( LIN o,c,c9 & LIN b9,q,c9 ) by A4, A13, A14, A25, AFF_1:6, AFF_1:21;
A33: ( b <> c & a <> p ) by A19, A20, A24, A26, AFF_1:7, AFF_1:14;
A34: ( a9 <> c9 & b <> a ) by A20, A21, AFF_1:7;
b <> a by A20, AFF_1:7;
then A35: Line (b,a) is being_line by AFF_1:def_3;
set M = Line (b,c);
A36: c in Line (b,c) by AFF_1:15;
then A37: Line (b,c) <> P by A3, A4, A6, A11, A13, A17, AFF_1:18;
b <> c by A20, AFF_1:7;
then A38: Line (b,c) is being_line by AFF_1:def_3;
A39: ( b in Line (b,c) & q in Line (b,c) ) by A24, AFF_1:15, AFF_1:def_2;
q <> b
proof
assume A40: q = b ; ::_thesis: contradiction
( not LIN b,c,a & c,a // q,p ) by A20, A26, AFF_1:4, AFF_1:6;
hence contradiction by A18, A22, A40, AFF_1:55; ::_thesis: verum
end;
then A41: q <> b9 by A3, A12, A38, A39, A37, AFF_1:18;
A42: b in Line (b,a) by AFF_1:15;
p <> b by A18, A20, A24, A26, AFF_1:55;
then A43: p <> b9 by A3, A12, A35, A42, A31, A29, AFF_1:18;
A44: not LIN b9,p,q
proof
set N = Line (p,q);
A45: Line (p,q) is being_line by A18, AFF_1:def_3;
assume LIN b9,p,q ; ::_thesis: contradiction
then LIN p,q,b9 by AFF_1:6;
then A46: b9 in Line (p,q) by AFF_1:def_2;
( q in Line (p,q) & LIN q,b9,c9 ) by A25, AFF_1:6, AFF_1:15;
then A47: c9 in Line (p,q) by A41, A45, A46, AFF_1:25;
( p in Line (p,q) & LIN p,b9,a9 ) by A23, AFF_1:6, AFF_1:15;
then a9 in Line (p,q) by A43, A45, A46, AFF_1:25;
hence contradiction by A21, A45, A46, A47, AFF_1:21; ::_thesis: verum
end;
Line (b,a) <> Line (b,c) by A20, A35, A42, A28, A36, AFF_1:21;
hence a,c // a9,c9 by A1, A3, A11, A12, A16, A26, A35, A38, A42, A28, A36, A31, A39, A37, A29, A34, A30, A44, A33, A27, A32, Def1; ::_thesis: verum
end;
theorem :: AFF_3:2
for AP being AffinPlane st AP is satisfying_DES1_1 holds
AP is satisfying_DES1
proof
let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES1_1 implies AP is satisfying_DES1 )
assume A1: AP is satisfying_DES1_1 ; ::_thesis: AP is satisfying_DES1
let A be Subset of AP; :: according to AFF_3:def_1 ::_thesis: for P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q
let P, C be Subset of AP; ::_thesis: for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q
let o, a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 implies a,c // p,q )
assume that
A2: A is being_line and
A3: P is being_line and
A4: C is being_line and
A5: P <> A and
A6: P <> C and
A7: A <> C and
A8: o in A and
A9: a in A and
A10: a9 in A and
A11: o in P and
A12: b in P and
A13: b9 in P and
A14: o in C and
A15: c in C and
A16: c9 in C and
A17: o <> a and
A18: o <> b and
A19: o <> c and
A20: p <> q and
A21: not LIN b,a,c and
A22: not LIN b9,a9,c9 and
A23: a <> a9 and
A24: LIN b,a,p and
A25: LIN b9,a9,p and
A26: LIN b,c,q and
A27: LIN b9,c9,q and
A28: a,c // a9,c9 ; ::_thesis: a,c // p,q
A29: a9 <> b9 by A22, AFF_1:7;
set M = Line (b,c);
A30: c in Line (b,c) by AFF_1:15;
then A31: Line (b,c) <> P by A3, A4, A6, A11, A14, A15, A19, AFF_1:18;
A32: Line (b,c) <> P by A3, A4, A6, A11, A14, A15, A19, A30, AFF_1:18;
A33: b in Line (b,c) by AFF_1:15;
set K = Line (b,a);
A34: a in Line (b,a) by AFF_1:15;
then A35: Line (b,a) <> P by A2, A3, A5, A8, A9, A11, A17, AFF_1:18;
A36: p in Line (b,a) by A24, AFF_1:def_2;
A37: ( a9 <> c9 & b <> a ) by A21, A22, AFF_1:7;
A38: b <> c by A21, AFF_1:7;
A39: q in Line (b,c) by A26, AFF_1:def_2;
A40: b9 <> c9 by A22, AFF_1:7;
A41: b in Line (b,a) by AFF_1:15;
A42: not LIN o,a,c
proof
assume LIN o,a,c ; ::_thesis: contradiction
then c in A by A2, A8, A9, A17, AFF_1:25;
hence contradiction by A2, A4, A7, A8, A14, A15, A19, AFF_1:18; ::_thesis: verum
end;
A43: c <> c9
proof
assume c = c9 ; ::_thesis: contradiction
then A44: c,a // c,a9 by A28, AFF_1:4;
( LIN o,a,a9 & not LIN o,c,a ) by A2, A8, A9, A10, A42, AFF_1:6, AFF_1:21;
hence contradiction by A23, A44, AFF_1:14; ::_thesis: verum
end;
b <> c by A21, AFF_1:7;
then A45: Line (b,c) is being_line by AFF_1:def_3;
b <> a by A21, AFF_1:7;
then A46: Line (b,a) is being_line by AFF_1:def_3;
A47: Line (b,a) <> P by A2, A3, A5, A8, A9, A11, A17, A34, AFF_1:18;
A48: now__::_thesis:_(_LIN_b9,p,q_implies_a,c_//_p,q_)
set C9 = Line (b9,c9);
set A9 = Line (b9,a9);
A49: c9 in Line (b9,c9) by AFF_1:15;
A50: ( Line (b9,a9) is being_line & b9 in Line (b9,a9) ) by A29, AFF_1:15, AFF_1:def_3;
A51: a9 in Line (b9,a9) by AFF_1:15;
then A52: Line (b9,a9) <> Line (b9,c9) by A22, A50, A49, AFF_1:21;
A53: q in Line (b9,c9) by A27, AFF_1:def_2;
A54: p in Line (b9,a9) by A25, AFF_1:def_2;
A55: ( Line (b9,c9) is being_line & b9 in Line (b9,c9) ) by A40, AFF_1:15, AFF_1:def_3;
assume A56: LIN b9,p,q ; ::_thesis: a,c // p,q
then A57: LIN b9,q,p by AFF_1:6;
A58: now__::_thesis:_(_b9_<>_q_implies_a,c_//_p,q_)
A59: Line (b9,c9) <> Line (b,c)
proof
assume Line (b9,c9) = Line (b,c) ; ::_thesis: contradiction
then LIN c,c9,b by A45, A33, A30, A49, AFF_1:21;
then b in C by A4, A15, A16, A43, AFF_1:25;
hence contradiction by A3, A4, A6, A11, A12, A14, A18, AFF_1:18; ::_thesis: verum
end;
assume b9 <> q ; ::_thesis: a,c // p,q
then A60: p in Line (b9,c9) by A57, A55, A53, AFF_1:25;
then LIN b,a,b9 by A24, A50, A54, A55, A52, AFF_1:18;
then b9 in Line (b,a) by AFF_1:def_2;
then A61: b = b9 by A3, A12, A13, A46, A41, A47, AFF_1:18;
p = b9 by A50, A54, A55, A52, A60, AFF_1:18;
then p = q by A45, A33, A39, A55, A53, A61, A59, AFF_1:18;
hence a,c // p,q by AFF_1:3; ::_thesis: verum
end;
now__::_thesis:_(_b9_<>_p_implies_a,c_//_p,q_)
A62: Line (b9,a9) <> Line (b,a)
proof
assume Line (b9,a9) = Line (b,a) ; ::_thesis: contradiction
then LIN a,a9,b by A46, A41, A34, A51, AFF_1:21;
then b in A by A2, A9, A10, A23, AFF_1:25;
hence contradiction by A2, A3, A5, A8, A11, A12, A18, AFF_1:18; ::_thesis: verum
end;
assume b9 <> p ; ::_thesis: a,c // p,q
then A63: q in Line (b9,a9) by A56, A50, A54, AFF_1:25;
then LIN b,c,b9 by A26, A50, A55, A53, A52, AFF_1:18;
then b9 in Line (b,c) by AFF_1:def_2;
then A64: b = b9 by A3, A12, A13, A45, A33, A32, AFF_1:18;
q = b9 by A50, A55, A53, A52, A63, AFF_1:18;
then p = q by A46, A41, A36, A50, A54, A64, A62, AFF_1:18;
hence a,c // p,q by AFF_1:3; ::_thesis: verum
end;
hence a,c // p,q by A20, A58; ::_thesis: verum
end;
A65: Line (b,a) <> Line (b,c) by A21, A46, A41, A34, A30, AFF_1:21;
now__::_thesis:_(_not_LIN_b9,p,q_implies_a,c_//_p,q_)
A66: ( LIN o,c,c9 & LIN b9,q,c9 ) by A4, A14, A15, A16, A27, AFF_1:6, AFF_1:21;
assume A67: not LIN b9,p,q ; ::_thesis: a,c // p,q
( LIN o,a,a9 & LIN b9,p,a9 ) by A2, A8, A9, A10, A25, AFF_1:6, AFF_1:21;
hence a,c // p,q by A1, A3, A11, A12, A13, A18, A28, A46, A45, A41, A34, A33, A30, A36, A39, A31, A35, A37, A38, A65, A42, A43, A67, A66, Def2; ::_thesis: verum
end;
hence a,c // p,q by A48; ::_thesis: verum
end;
theorem :: AFF_3:3
for AP being AffinPlane st AP is Desarguesian holds
AP is satisfying_DES1
proof
let AP be AffinPlane; ::_thesis: ( AP is Desarguesian implies AP is satisfying_DES1 )
assume A1: AP is Desarguesian ; ::_thesis: AP is satisfying_DES1
let A be Subset of AP; :: according to AFF_3:def_1 ::_thesis: for P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q
let P, C be Subset of AP; ::_thesis: for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q
let o, a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 implies a,c // p,q )
assume that
A2: A is being_line and
A3: P is being_line and
A4: C is being_line and
A5: P <> A and
A6: P <> C and
A7: A <> C and
A8: o in A and
A9: a in A and
A10: a9 in A and
A11: o in P and
A12: b in P and
A13: b9 in P and
A14: o in C and
A15: c in C and
A16: c9 in C and
A17: o <> a and
A18: o <> b and
A19: o <> c and
p <> q and
A20: not LIN b,a,c and
A21: not LIN b9,a9,c9 and
A22: a <> a9 and
A23: LIN b,a,p and
A24: LIN b9,a9,p and
A25: LIN b,c,q and
A26: LIN b9,c9,q and
A27: a,c // a9,c9 ; ::_thesis: a,c // p,q
set D = Line (b,c);
b <> c by A20, AFF_1:7;
then Line (b,c) is being_line by AFF_1:def_3;
then consider D9 being Subset of AP such that
A28: c9 in D9 and
A29: Line (b,c) // D9 by AFF_1:49;
A30: D9 is being_line by A29, AFF_1:36;
set M = Line (b9,c9);
A31: q in Line (b9,c9) by A26, AFF_1:def_2;
A32: b in Line (b,c) by AFF_1:15;
A33: c in Line (b,c) by AFF_1:15;
not D9 // P
proof
assume D9 // P ; ::_thesis: contradiction
then Line (b,c) // P by A29, AFF_1:44;
then c in P by A12, A32, A33, AFF_1:45;
hence contradiction by A3, A4, A6, A11, A14, A15, A19, AFF_1:18; ::_thesis: verum
end;
then consider d being Element of AP such that
A34: d in D9 and
A35: d in P by A3, A30, AFF_1:58;
A36: q in Line (b,c) by A25, AFF_1:def_2;
then A37: d,c9 // b,q by A32, A28, A29, A34, AFF_1:39;
A38: ( a <> b & b,a // b,p ) by A20, A23, AFF_1:7, AFF_1:def_1;
A39: c,a // c9,a9 by A27, AFF_1:4;
c,b // c9,d by A32, A33, A28, A29, A34, AFF_1:39;
then b,a // d,a9 by A1, A2, A3, A4, A6, A7, A8, A9, A10, A11, A12, A14, A15, A16, A17, A18, A19, A35, A39, AFF_2:def_4;
then A40: d,a9 // b,p by A38, AFF_1:5;
set K = Line (b9,a9);
A41: ( b9 in Line (b9,a9) & p in Line (b9,a9) ) by A24, AFF_1:15, AFF_1:def_2;
A42: a9 <> b9 by A21, AFF_1:7;
then A43: Line (b9,a9) is being_line by AFF_1:def_3;
A44: b9 in Line (b9,c9) by AFF_1:15;
A45: c9 in Line (b9,c9) by AFF_1:15;
A46: b9 <> c9 by A21, AFF_1:7;
then A47: Line (b9,c9) is being_line by AFF_1:def_3;
A48: not LIN o,a,c
proof
assume LIN o,a,c ; ::_thesis: contradiction
then c in A by A2, A8, A9, A17, AFF_1:25;
hence contradiction by A2, A4, A7, A8, A14, A15, A19, AFF_1:18; ::_thesis: verum
end;
A49: c <> c9
proof
assume c = c9 ; ::_thesis: contradiction
then A50: c,a // c,a9 by A27, AFF_1:4;
( LIN o,a,a9 & not LIN o,c,a ) by A2, A8, A9, A10, A48, AFF_1:6, AFF_1:21;
hence contradiction by A22, A50, AFF_1:14; ::_thesis: verum
end;
A51: d <> b9
proof
assume d = b9 ; ::_thesis: contradiction
then Line (b9,c9) = D9 by A46, A47, A44, A45, A28, A30, A34, AFF_1:18;
then Line (b,c) = Line (b9,c9) by A31, A36, A29, AFF_1:45;
then LIN c,c9,b by A47, A45, A32, A33, AFF_1:21;
then b in C by A4, A15, A16, A49, AFF_1:25;
hence contradiction by A3, A4, A6, A11, A12, A14, A18, AFF_1:18; ::_thesis: verum
end;
A52: a9 <> c9 by A21, AFF_1:7;
A53: o <> a9
proof
assume A54: o = a9 ; ::_thesis: contradiction
LIN o,c,c9 by A4, A14, A15, A16, AFF_1:21;
hence contradiction by A27, A52, A48, A54, AFF_1:55; ::_thesis: verum
end;
o <> c9
proof
A55: not LIN o,c,a by A48, AFF_1:6;
assume A56: o = c9 ; ::_thesis: contradiction
( LIN o,a,a9 & c,a // c9,a9 ) by A2, A8, A9, A10, A27, AFF_1:4, AFF_1:21;
hence contradiction by A53, A56, A55, AFF_1:55; ::_thesis: verum
end;
then A57: Line (b9,c9) <> P by A3, A4, A6, A11, A14, A16, A45, AFF_1:18;
A58: a9 in Line (b9,a9) by AFF_1:15;
then Line (b9,a9) <> P by A2, A3, A5, A8, A10, A11, A53, AFF_1:18;
then a9,c9 // p,q by A1, A3, A12, A13, A42, A46, A43, A47, A58, A41, A44, A45, A31, A57, A35, A51, A40, A37, AFF_2:def_4;
hence a,c // p,q by A27, A52, AFF_1:5; ::_thesis: verum
end;
theorem :: AFF_3:4
for AP being AffinPlane st AP is Desarguesian holds
AP is satisfying_DES1_2
proof
let AP be AffinPlane; ::_thesis: ( AP is Desarguesian implies AP is satisfying_DES1_2 )
assume A1: AP is Desarguesian ; ::_thesis: AP is satisfying_DES1_2
then A2: AP is satisfying_DES_1 by AFF_2:2;
let A be Subset of AP; :: according to AFF_3:def_3 ::_thesis: for P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
o in C
let P, C be Subset of AP; ::_thesis: for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
o in C
let o, a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q implies o in C )
assume that
A3: A is being_line and
A4: P is being_line and
A5: C is being_line and
A6: P <> A and
A7: P <> C and
A <> C and
A8: o in A and
A9: ( a in A & a9 in A ) and
A10: o in P and
A11: b in P and
A12: b9 in P and
A13: c in C and
A14: c9 in C and
A15: o <> a and
A16: o <> b and
o <> c and
A17: p <> q and
A18: not LIN b,a,c and
A19: not LIN b9,a9,c9 and
A20: c <> c9 and
A21: LIN b,a,p and
A22: LIN b9,a9,p and
A23: LIN b,c,q and
A24: LIN b9,c9,q and
A25: a,c // a9,c9 and
A26: a,c // p,q ; ::_thesis: o in C
A27: b <> p by A17, A18, A23, A26, AFF_1:55;
set K = Line (b9,a9);
A28: p in Line (b9,a9) by A22, AFF_1:def_2;
a9 <> b9 by A19, AFF_1:7;
then A29: Line (b9,a9) is being_line by AFF_1:def_3;
A30: b <> q
proof
assume A31: b = q ; ::_thesis: contradiction
( not LIN b,c,a & c,a // q,p ) by A18, A26, AFF_1:4, AFF_1:6;
hence contradiction by A17, A21, A31, AFF_1:55; ::_thesis: verum
end;
set M = Line (b9,c9);
A32: q in Line (b9,c9) by A24, AFF_1:def_2;
A33: c9 in Line (b9,c9) by AFF_1:15;
A34: a <> c by A18, AFF_1:7;
A35: b9 <> p
proof
assume A36: b9 = p ; ::_thesis: contradiction
a9,c9 // p,q by A25, A26, A34, AFF_1:5;
hence contradiction by A17, A19, A24, A36, AFF_1:55; ::_thesis: verum
end;
A37: b9 <> q
proof
a9,c9 // p,q by A25, A26, A34, AFF_1:5;
then A38: c9,a9 // q,p by AFF_1:4;
assume A39: b9 = q ; ::_thesis: contradiction
not LIN b9,c9,a9 by A19, AFF_1:6;
hence contradiction by A17, A22, A39, A38, AFF_1:55; ::_thesis: verum
end;
A40: b <> c by A18, AFF_1:7;
A41: a <> b by A18, AFF_1:7;
A42: ( b9 <> a9 & b9 <> c9 ) by A19, AFF_1:7;
A43: a9 in Line (b9,a9) by AFF_1:15;
A44: b9 in Line (b9,c9) by AFF_1:15;
A45: b9 <> c9 by A19, AFF_1:7;
then A46: Line (b9,c9) is being_line by AFF_1:def_3;
A47: b9 in Line (b9,a9) by AFF_1:15;
then A48: Line (b9,a9) <> Line (b9,c9) by A19, A29, A43, A33, AFF_1:21;
now__::_thesis:_o_in_C
A49: now__::_thesis:_(_Line_(b9,c9)_<>_P_implies_o_in_C_)
p,q // a9,c9 by A25, A26, A34, AFF_1:5;
then A50: c9,a9 // q,p by AFF_1:4;
A51: b,a // b,p by A21, AFF_1:def_1;
set D = Line (b,c);
A52: b in Line (b,c) by AFF_1:15;
Line (b,c) is being_line by A40, AFF_1:def_3;
then consider D9 being Subset of AP such that
A53: c9 in D9 and
A54: Line (b,c) // D9 by AFF_1:49;
A55: D9 is being_line by A54, AFF_1:36;
A56: q in Line (b,c) by A23, AFF_1:def_2;
assume A57: Line (b9,c9) <> P ; ::_thesis: o in C
not D9 // P
proof
assume D9 // P ; ::_thesis: contradiction
then Line (b,c) // P by A54, AFF_1:44;
then q in P by A11, A52, A56, AFF_1:45;
hence contradiction by A4, A12, A46, A44, A32, A37, A57, AFF_1:18; ::_thesis: verum
end;
then consider d being Element of AP such that
A58: d in D9 and
A59: d in P by A4, A55, AFF_1:58;
A60: c in Line (b,c) by AFF_1:15;
A61: d <> b9
proof
assume d = b9 ; ::_thesis: contradiction
then Line (b9,c9) = D9 by A45, A46, A44, A33, A53, A55, A58, AFF_1:18;
then A62: Line (b,c) = Line (b9,c9) by A32, A56, A54, AFF_1:45;
then LIN c,c9,b by A46, A33, A52, A60, AFF_1:21;
then A63: b in C by A5, A13, A14, A20, AFF_1:25;
set N = Line (a,c);
set T = Line (b,a);
A64: b in Line (b,a) by AFF_1:15;
A65: c in Line (a,c) by AFF_1:15;
A66: a in Line (b,a) by AFF_1:15;
A67: Line (a,c) is being_line by A34, AFF_1:def_3;
A68: a in Line (a,c) by AFF_1:15;
A69: a <> a9
proof
assume a = a9 ; ::_thesis: contradiction
then LIN a,c,c9 by A25, AFF_1:def_1;
then c9 in Line (a,c) by AFF_1:def_2;
then Line (a,c) = C by A5, A13, A14, A20, A67, A65, AFF_1:18;
hence contradiction by A13, A18, A63, A67, A68, AFF_1:21; ::_thesis: verum
end;
A70: ( Line (b,a) is being_line & p in Line (b,a) ) by A21, A41, AFF_1:def_2, AFF_1:def_3;
A71: b <> b9
proof
A72: Line (b9,a9) <> Line (b,a)
proof
assume Line (b9,a9) = Line (b,a) ; ::_thesis: contradiction
then Line (b,a) = A by A3, A9, A29, A43, A66, A69, AFF_1:18;
hence contradiction by A3, A4, A6, A8, A10, A11, A16, A64, AFF_1:18; ::_thesis: verum
end;
assume b = b9 ; ::_thesis: contradiction
hence contradiction by A29, A47, A28, A35, A64, A70, A72, AFF_1:18; ::_thesis: verum
end;
LIN c,c9,b9 by A46, A44, A33, A60, A62, AFF_1:21;
then b9 in C by A5, A13, A14, A20, AFF_1:25;
hence contradiction by A4, A5, A7, A11, A12, A63, A71, AFF_1:18; ::_thesis: verum
end;
c9,d // q,b by A52, A56, A53, A54, A58, AFF_1:39;
then d,a9 // b,p by A1, A4, A11, A12, A42, A29, A46, A47, A43, A28, A44, A33, A32, A48, A57, A59, A61, A50, AFF_2:def_4;
then A73: b,a // d,a9 by A27, A51, AFF_1:5;
b,c // d,c9 by A52, A60, A53, A54, A58, AFF_1:39;
hence o in C by A2, A3, A4, A5, A6, A8, A9, A10, A11, A13, A14, A15, A16, A18, A20, A25, A59, A73, AFF_2:def_5; ::_thesis: verum
end;
now__::_thesis:_(_Line_(b9,c9)_=_P_implies_o_in_C_)
assume A74: Line (b9,c9) = P ; ::_thesis: o in C
LIN b,q,c by A23, AFF_1:6;
then c in P by A11, A46, A32, A30, A74, AFF_1:25;
then P = Line (c,c9) by A20, A46, A33, A74, AFF_1:57;
hence o in C by A5, A10, A13, A14, A20, AFF_1:57; ::_thesis: verum
end;
hence o in C by A49; ::_thesis: verum
end;
hence o in C ; ::_thesis: verum
end;
theorem :: AFF_3:5
for AP being AffinPlane st AP is satisfying_DES1_2 holds
AP is satisfying_DES1_3
proof
let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES1_2 implies AP is satisfying_DES1_3 )
assume A1: AP is satisfying_DES1_2 ; ::_thesis: AP is satisfying_DES1_3
let A be Subset of AP; :: according to AFF_3:def_4 ::_thesis: for P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & b <> b9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
o in P
let P, C be Subset of AP; ::_thesis: for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & b <> b9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
o in P
let o, a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & b <> b9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q implies o in P )
assume that
A2: A is being_line and
A3: P is being_line and
A4: C is being_line and
A5: P <> A and
A6: P <> C and
A7: A <> C and
A8: o in A and
A9: a in A and
A10: a9 in A and
A11: b in P and
A12: b9 in P and
A13: o in C and
A14: c in C and
A15: c9 in C and
A16: o <> a and
A17: o <> b and
A18: o <> c and
A19: p <> q and
A20: not LIN b,a,c and
A21: not LIN b9,a9,c9 and
A22: b <> b9 and
A23: a <> a9 and
A24: LIN b,a,p and
A25: LIN b9,a9,p and
A26: LIN b,c,q and
A27: LIN b9,c9,q and
A28: a,c // a9,c9 and
A29: a,c // p,q ; ::_thesis: o in P
set D = Line (b,c);
set K = Line (b9,a9);
assume A30: not o in P ; ::_thesis: contradiction
A31: not LIN o,c,a
proof
assume LIN o,c,a ; ::_thesis: contradiction
then a in C by A4, A13, A14, A18, AFF_1:25;
hence contradiction by A2, A4, A7, A8, A9, A13, A16, AFF_1:18; ::_thesis: verum
end;
A32: c <> c9
proof
assume c = c9 ; ::_thesis: contradiction
then A33: c,a // c,a9 by A28, AFF_1:4;
LIN o,a,a9 by A2, A8, A9, A10, AFF_1:21;
hence contradiction by A23, A31, A33, AFF_1:14; ::_thesis: verum
end;
a <> c by A20, AFF_1:7;
then A34: a9,c9 // p,q by A28, A29, AFF_1:5;
A35: ( p <> b & p <> b9 & q <> b & q <> b9 )
proof
A36: now__::_thesis:_not_b9_=_q
assume A37: b9 = q ; ::_thesis: contradiction
( not LIN b9,c9,a9 & c9,a9 // q,p ) by A21, A34, AFF_1:4, AFF_1:6;
hence contradiction by A19, A25, A37, AFF_1:55; ::_thesis: verum
end;
A38: now__::_thesis:_not_b_=_q
assume A39: b = q ; ::_thesis: contradiction
( not LIN b,c,a & c,a // q,p ) by A20, A29, AFF_1:4, AFF_1:6;
hence contradiction by A19, A24, A39, AFF_1:55; ::_thesis: verum
end;
assume ( not p <> b or not p <> b9 or not q <> b or not q <> b9 ) ; ::_thesis: contradiction
hence contradiction by A20, A21, A26, A27, A29, A34, A38, A36, AFF_1:55; ::_thesis: verum
end;
A40: b <> c by A20, AFF_1:7;
then A41: ( Line (b,c) is being_line & c in Line (b,c) ) by AFF_1:24;
A42: b in Line (b,c) by A40, AFF_1:24;
then A43: q in Line (b,c) by A26, A40, A41, AFF_1:25;
A44: now__::_thesis:_C_//_P
assume not C // P ; ::_thesis: contradiction
then consider x being Element of AP such that
A45: x in C and
A46: x in P by A3, A4, AFF_1:58;
A47: x <> c
proof
A48: ( LIN q,b9,c9 & LIN q,b9,b9 ) by A27, AFF_1:6, AFF_1:7;
assume A49: x = c ; ::_thesis: contradiction
then ( LIN b,c,b9 & LIN b,c,c ) by A3, A11, A12, A46, AFF_1:21;
then LIN q,b9,c by A26, A40, AFF_1:8;
then A50: b9 in C by A4, A14, A15, A32, A35, A48, AFF_1:8, AFF_1:25;
then LIN c,c9,q by A3, A4, A6, A12, A14, A27, A46, A49, AFF_1:18;
then A51: q in C by A4, A14, A15, A32, AFF_1:25;
c = b9 by A3, A4, A6, A12, A14, A46, A49, A50, AFF_1:18;
then C = Line (b,c) by A4, A14, A35, A41, A43, A51, AFF_1:18;
hence contradiction by A3, A4, A6, A11, A12, A22, A42, A50, AFF_1:18; ::_thesis: verum
end;
A52: x <> b
proof
A53: LIN q,c9,b9 by A27, AFF_1:6;
assume A54: x = b ; ::_thesis: contradiction
then q in C by A4, A14, A26, A40, A45, AFF_1:25;
then ( q = c9 or b9 in C ) by A4, A15, A53, AFF_1:25;
then c9,a9 // c9,p by A3, A4, A6, A11, A12, A22, A34, A45, A54, AFF_1:4, AFF_1:18;
then LIN c9,a9,p by AFF_1:def_1;
then A55: LIN p,a9,c9 by AFF_1:6;
( LIN p,a9,b9 & LIN p,a9,a9 ) by A25, AFF_1:6, AFF_1:7;
then p = a9 by A21, A55, AFF_1:8;
then LIN a,a9,b by A24, AFF_1:6;
then b in A by A2, A9, A10, A23, AFF_1:25;
hence contradiction by A2, A4, A7, A8, A13, A17, A45, A54, AFF_1:18; ::_thesis: verum
end;
A56: ( c,a // q,p & c,a // c9,a9 ) by A28, A29, AFF_1:4;
( not LIN b,c,a & not LIN b9,c9,a9 ) by A20, A21, AFF_1:6;
then x in A by A1, A2, A3, A4, A6, A9, A10, A11, A12, A14, A15, A19, A23, A24, A25, A26, A27, A45, A46, A47, A52, A56, Def3;
hence contradiction by A2, A4, A7, A8, A13, A30, A45, A46, AFF_1:18; ::_thesis: verum
end;
A57: a <> b by A20, AFF_1:7;
A58: a9 <> b9 by A21, AFF_1:7;
then A59: a9 in Line (b9,a9) by AFF_1:24;
A60: ( Line (b9,a9) is being_line & b9 in Line (b9,a9) ) by A58, AFF_1:24;
then A61: p in Line (b9,a9) by A25, A58, A59, AFF_1:25;
A62: now__::_thesis:_P_//_A
assume not P // A ; ::_thesis: contradiction
then consider x being Element of AP such that
A63: x in P and
A64: x in A by A2, A3, AFF_1:58;
A65: x <> b
proof
assume A66: x = b ; ::_thesis: contradiction
then p in A by A2, A9, A24, A57, A64, AFF_1:25;
then ( a9,c9 // a9,q or b9 in A ) by A2, A10, A34, A60, A59, A61, AFF_1:18;
then LIN a9,c9,q by A2, A3, A5, A11, A12, A22, A64, A66, AFF_1:18, AFF_1:def_1;
then A67: LIN q,c9,a9 by AFF_1:6;
( LIN q,c9,b9 & LIN q,c9,c9 ) by A27, AFF_1:6, AFF_1:7;
then q = c9 by A21, A67, AFF_1:8;
then LIN c,c9,b by A26, AFF_1:6;
then b in C by A4, A14, A15, A32, AFF_1:25;
hence contradiction by A2, A4, A7, A8, A13, A17, A64, A66, AFF_1:18; ::_thesis: verum
end;
x <> a
proof
assume x = a ; ::_thesis: contradiction
then ( p in P & Line (b9,a9) <> P ) by A2, A3, A5, A9, A10, A11, A23, A24, A57, A59, A63, AFF_1:18, AFF_1:25;
hence contradiction by A3, A12, A35, A60, A61, AFF_1:18; ::_thesis: verum
end;
then x in C by A1, A2, A3, A4, A5, A9, A10, A11, A12, A14, A15, A19, A20, A21, A24, A25, A26, A27, A28, A29, A32, A63, A64, A65, Def3;
hence contradiction by A2, A4, A7, A8, A13, A30, A63, A64, AFF_1:18; ::_thesis: verum
end;
( not P // A or not C // P )
proof
assume ( P // A & C // P ) ; ::_thesis: contradiction
then C // A by AFF_1:44;
hence contradiction by A7, A8, A13, AFF_1:45; ::_thesis: verum
end;
hence contradiction by A62, A44; ::_thesis: verum
end;
theorem :: AFF_3:6
for AP being AffinPlane st AP is satisfying_DES1_2 holds
AP is Desarguesian
proof
let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES1_2 implies AP is Desarguesian )
assume A1: AP is satisfying_DES1_2 ; ::_thesis: AP is Desarguesian
let A be Subset of AP; :: according to AFF_2:def_4 ::_thesis: for b1, b2 being M2(K24( the U1 of AP))
for b3, b4, b5, b6, b7, b8, b9 being M2( the U1 of AP) holds
( not b3 in A or not b3 in b1 or not b3 in b2 or b3 = b4 or b3 = b5 or b3 = b6 or not b4 in A or not b7 in A or not b5 in b1 or not b8 in b1 or not b6 in b2 or not b9 in b2 or not A is being_line or not b1 is being_line or not b2 is being_line or A = b1 or A = b2 or not b4,b5 // b7,b8 or not b4,b6 // b7,b9 or b5,b6 // b8,b9 )
let P, C be Subset of AP; ::_thesis: for b1, b2, b3, b4, b5, b6, b7 being M2( the U1 of AP) holds
( not b1 in A or not b1 in P or not b1 in C or b1 = b2 or b1 = b3 or b1 = b4 or not b2 in A or not b5 in A or not b3 in P or not b6 in P or not b4 in C or not b7 in C or not A is being_line or not P is being_line or not C is being_line or A = P or A = C or not b2,b3 // b5,b6 or not b2,b4 // b5,b7 or b3,b4 // b6,b7 )
let o, a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( not o in A or not o in P or not o in C or o = a or o = b or o = c or not a in A or not a9 in A or not b in P or not b9 in P or not c in C or not c9 in C or not A is being_line or not P is being_line or not C is being_line or A = P or A = C or not a,b // a9,b9 or not a,c // a9,c9 or b,c // b9,c9 )
assume that
A2: o in A and
A3: o in P and
A4: o in C and
A5: o <> a and
A6: o <> b and
A7: o <> c and
A8: a in A and
A9: a9 in A and
A10: b in P and
A11: b9 in P and
A12: c in C and
A13: c9 in C and
A14: A is being_line and
A15: P is being_line and
A16: C is being_line and
A17: A <> P and
A18: A <> C and
A19: a,b // a9,b9 and
A20: a,c // a9,c9 ; ::_thesis: b,c // b9,c9
now__::_thesis:_(_P_<>_C_implies_b,c_//_b9,c9_)
A21: ( not LIN o,b,a & not LIN o,a,c )
proof
A22: now__::_thesis:_not_LIN_o,a,c
assume LIN o,a,c ; ::_thesis: contradiction
then c in A by A2, A5, A8, A14, AFF_1:25;
hence contradiction by A2, A4, A7, A12, A14, A16, A18, AFF_1:18; ::_thesis: verum
end;
A23: now__::_thesis:_not_LIN_o,b,a
assume LIN o,b,a ; ::_thesis: contradiction
then a in P by A3, A6, A10, A15, AFF_1:25;
hence contradiction by A2, A3, A5, A8, A14, A15, A17, AFF_1:18; ::_thesis: verum
end;
assume ( LIN o,b,a or LIN o,a,c ) ; ::_thesis: contradiction
hence contradiction by A23, A22; ::_thesis: verum
end;
A24: ( b = b9 implies b,c // b9,c9 )
proof
A25: LIN o,c,c9 by A4, A12, A13, A16, AFF_1:21;
A26: LIN o,a,a9 by A2, A8, A9, A14, AFF_1:21;
assume A27: b = b9 ; ::_thesis: b,c // b9,c9
then b,a // b,a9 by A19, AFF_1:4;
then a,c // a,c9 by A20, A21, A26, AFF_1:14;
then c = c9 by A21, A25, AFF_1:14;
hence b,c // b9,c9 by A27, AFF_1:2; ::_thesis: verum
end;
A28: ( a9 = o implies b,c // b9,c9 )
proof
assume A29: a9 = o ; ::_thesis: b,c // b9,c9
( LIN o,b,b9 & not LIN o,a,b ) by A3, A10, A11, A15, A21, AFF_1:6, AFF_1:21;
then A30: o = b9 by A19, A29, AFF_1:55;
LIN o,c,c9 by A4, A12, A13, A16, AFF_1:21;
then o = c9 by A20, A21, A29, AFF_1:55;
hence b,c // b9,c9 by A30, AFF_1:3; ::_thesis: verum
end;
A31: ( c9 = o implies b,c // b9,c9 )
proof
A32: c,a // c9,a9 by A20, AFF_1:4;
assume A33: c9 = o ; ::_thesis: b,c // b9,c9
( LIN o,a,a9 & not LIN o,c,a ) by A2, A8, A9, A14, A21, AFF_1:6, AFF_1:21;
hence b,c // b9,c9 by A28, A33, A32, AFF_1:55; ::_thesis: verum
end;
set K = Line (a,c);
A34: a in Line (a,c) by AFF_1:15;
A35: a <> c by A2, A4, A5, A8, A12, A14, A16, A18, AFF_1:18;
then A36: Line (a,c) is being_line by AFF_1:def_3;
A37: c in Line (a,c) by AFF_1:15;
A38: a <> b by A2, A3, A5, A8, A10, A14, A15, A17, AFF_1:18;
A39: ( LIN a,b,c implies b,c // b9,c9 )
proof
consider N being Subset of AP such that
A40: a9 in N and
A41: Line (a,c) // N by A36, AFF_1:49;
A42: N is being_line by A41, AFF_1:36;
a9,c9 // Line (a,c) by A20, A35, AFF_1:29, AFF_1:32;
then a9,c9 // N by A41, AFF_1:43;
then A43: c9 in N by A40, A42, AFF_1:23;
assume LIN a,b,c ; ::_thesis: b,c // b9,c9
then LIN a,c,b by AFF_1:6;
then A44: b in Line (a,c) by AFF_1:def_2;
then Line (a,c) = Line (a,b) by A38, A36, A34, AFF_1:57;
then a9,b9 // Line (a,c) by A19, A38, AFF_1:29, AFF_1:32;
then a9,b9 // N by A41, AFF_1:43;
then b9 in N by A40, A42, AFF_1:23;
hence b,c // b9,c9 by A37, A44, A41, A43, AFF_1:39; ::_thesis: verum
end;
assume A45: P <> C ; ::_thesis: b,c // b9,c9
A46: now__::_thesis:_(_o_<>_a9_&_o_<>_b9_&_o_<>_c9_&_b_<>_b9_&_not_LIN_a,b,c_implies_b,c_//_b9,c9_)
set T = Line (b9,a9);
set D = Line (b,a);
set N = Line (a9,c9);
assume that
A47: o <> a9 and
A48: o <> b9 and
A49: o <> c9 and
A50: b <> b9 and
A51: not LIN a,b,c ; ::_thesis: b,c // b9,c9
A52: c9 in Line (a9,c9) by AFF_1:15;
assume not b,c // b9,c9 ; ::_thesis: contradiction
then consider q being Element of AP such that
A53: LIN b,c,q and
A54: LIN b9,c9,q by AFF_1:60;
consider M being Subset of AP such that
A55: q in M and
A56: Line (a,c) // M by A36, AFF_1:49;
A57: M is being_line by A56, AFF_1:36;
not a,b // M
proof
assume a,b // M ; ::_thesis: contradiction
then a,b // Line (a,c) by A56, AFF_1:43;
then b in Line (a,c) by A36, A34, AFF_1:23;
hence contradiction by A36, A34, A37, A51, AFF_1:21; ::_thesis: verum
end;
then consider p being Element of AP such that
A58: p in M and
A59: LIN a,b,p by A57, AFF_1:59;
A60: a9 in Line (a9,c9) by AFF_1:15;
A61: p <> q
proof
A62: ( LIN p,b,a & LIN p,b,b ) by A59, AFF_1:6, AFF_1:7;
assume A63: p = q ; ::_thesis: contradiction
then LIN p,b,c by A53, AFF_1:6;
then p = b by A51, A62, AFF_1:8;
then LIN b,b9,c9 by A54, A63, AFF_1:6;
then c9 in P by A10, A11, A15, A50, AFF_1:25;
hence contradiction by A3, A4, A13, A15, A16, A45, A49, AFF_1:18; ::_thesis: verum
end;
A64: c,a // q,p by A34, A37, A55, A56, A58, AFF_1:39;
A65: LIN b,a,p by A59, AFF_1:6;
A66: b9 <> c9 by A3, A4, A11, A13, A15, A16, A45, A48, AFF_1:18;
A67: a9 <> c9 by A2, A4, A9, A13, A14, A16, A18, A47, AFF_1:18;
then A68: Line (a9,c9) is being_line by AFF_1:def_3;
A69: Line (a,c) // Line (a9,c9) by A20, A35, A67, AFF_1:37;
then A70: Line (a9,c9) // M by A56, AFF_1:44;
A71: a9 <> b9 by A2, A3, A9, A11, A14, A15, A17, A47, AFF_1:18;
A72: not LIN a9,b9,c9
proof
assume LIN a9,b9,c9 ; ::_thesis: contradiction
then LIN a9,c9,b9 by AFF_1:6;
then b9 in Line (a9,c9) by AFF_1:def_2;
then a9,b9 // Line (a9,c9) by A68, A60, AFF_1:23;
then A73: a9,b9 // Line (a,c) by A69, AFF_1:43;
a9,b9 // a,b by A19, AFF_1:4;
then a,b // Line (a,c) by A71, A73, AFF_1:32;
then b in Line (a,c) by A36, A34, AFF_1:23;
hence contradiction by A36, A34, A37, A51, AFF_1:21; ::_thesis: verum
end;
not b9,p // Line (a9,c9)
proof
assume b9,p // Line (a9,c9) ; ::_thesis: contradiction
then b9,p // M by A70, AFF_1:43;
then p,b9 // M by AFF_1:34;
then A74: b9 in M by A57, A58, AFF_1:23;
A75: now__::_thesis:_not_b9_<>_q
assume A76: b9 <> q ; ::_thesis: contradiction
LIN b9,q,c9 by A54, AFF_1:6;
then c9 in M by A55, A57, A74, A76, AFF_1:25;
then ( a9 in Line (a9,c9) & b9 in Line (a9,c9) ) by A52, A70, A74, AFF_1:15, AFF_1:45;
hence contradiction by A68, A52, A72, AFF_1:21; ::_thesis: verum
end;
now__::_thesis:_not_b9_=_q
assume b9 = q ; ::_thesis: contradiction
then LIN b,b9,c by A53, AFF_1:6;
then c in P by A10, A11, A15, A50, AFF_1:25;
hence contradiction by A3, A4, A7, A12, A15, A16, A45, AFF_1:18; ::_thesis: verum
end;
hence contradiction by A75; ::_thesis: verum
end;
then consider x being Element of AP such that
A77: x in Line (a9,c9) and
A78: LIN b9,p,x by A68, AFF_1:59;
set A9 = Line (x,a);
A79: a <> a9
proof
assume A80: a = a9 ; ::_thesis: contradiction
( not LIN o,a,b & LIN o,b,b9 ) by A3, A10, A11, A15, A21, AFF_1:6, AFF_1:21;
hence contradiction by A19, A50, A80, AFF_1:14; ::_thesis: verum
end;
A81: x <> a
proof
assume x = a ; ::_thesis: contradiction
then a9 in Line (a,c) by A34, A60, A69, A77, AFF_1:45;
then A = Line (a,c) by A8, A9, A14, A36, A34, A79, AFF_1:18;
hence contradiction by A2, A4, A7, A12, A14, A16, A18, A37, AFF_1:18; ::_thesis: verum
end;
then A82: Line (x,a) is being_line by AFF_1:def_3;
A83: c <> c9
proof
assume c = c9 ; ::_thesis: contradiction
then A84: c,a // c,a9 by A20, AFF_1:4;
( not LIN o,c,a & LIN o,a,a9 ) by A2, A8, A9, A14, A21, AFF_1:6, AFF_1:21;
hence contradiction by A79, A84, AFF_1:14; ::_thesis: verum
end;
A85: not LIN b9,c9,x
proof
A86: now__::_thesis:_(_c9_=_x_implies_LIN_b9,c9,a9_)
A87: now__::_thesis:_not_q_=_c9
assume q = c9 ; ::_thesis: contradiction
then LIN c,c9,b by A53, AFF_1:6;
then b in C by A12, A13, A16, A83, AFF_1:25;
hence contradiction by A3, A4, A6, A10, A15, A16, A45, AFF_1:18; ::_thesis: verum
end;
assume c9 = x ; ::_thesis: LIN b9,c9,a9
then A88: LIN b9,c9,p by A78, AFF_1:6;
LIN b9,c9,c9 by AFF_1:7;
then c9 in M by A66, A54, A55, A57, A58, A61, A88, AFF_1:8, AFF_1:25;
then A89: q in Line (a9,c9) by A55, A52, A70, AFF_1:45;
LIN q,c9,b9 by A54, AFF_1:6;
then ( q = c9 or b9 in Line (a9,c9) ) by A68, A52, A89, AFF_1:25;
hence LIN b9,c9,a9 by A68, A60, A52, A87, AFF_1:21; ::_thesis: verum
end;
assume LIN b9,c9,x ; ::_thesis: contradiction
then A90: LIN c9,x,b9 by AFF_1:6;
A91: ( LIN c9,x,a9 & LIN c9,x,c9 ) by A68, A60, A52, A77, AFF_1:21;
then LIN c9,a9,b9 by A90, A86, AFF_1:6, AFF_1:8;
then c9,a9 // c9,b9 by AFF_1:def_1;
then a9,c9 // b9,c9 by AFF_1:4;
then A92: a,c // b9,c9 by A20, A67, AFF_1:5;
( c9 = x or LIN b9,c9,a9 ) by A90, A91, AFF_1:8;
then b9,c9 // b9,a9 by A86, AFF_1:def_1;
then b9,c9 // a9,b9 by AFF_1:4;
then b9,c9 // a,b by A19, A71, AFF_1:5;
then a,c // a,b by A66, A92, AFF_1:5;
then LIN a,c,b by AFF_1:def_1;
hence contradiction by A51, AFF_1:6; ::_thesis: verum
end;
A93: ( x in Line (x,a) & a in Line (x,a) ) by AFF_1:15;
A <> Line (a,c) by A2, A4, A7, A12, A14, A16, A18, A37, AFF_1:18;
then A94: A <> Line (a9,c9) by A8, A34, A69, AFF_1:45;
A95: not LIN b,c,a by A51, AFF_1:6;
A96: p in Line (b,a) by A59, AFF_1:def_2;
A97: ( Line (b,a) is being_line & b in Line (b,a) ) by A38, AFF_1:15, AFF_1:def_3;
A98: LIN b9,x,p by A78, AFF_1:6;
c,a // c9,x by A34, A37, A52, A69, A77, AFF_1:39;
then o in Line (x,a) by A1, A3, A4, A6, A7, A10, A11, A12, A13, A15, A16, A45, A53, A54, A98, A81, A82, A93, A61, A85, A64, A95, A65, Def3;
then x in A by A2, A5, A8, A14, A82, A93, AFF_1:18;
then x = a9 by A9, A14, A68, A60, A77, A94, AFF_1:18;
then A99: ( a9 in Line (b9,a9) & p in Line (b9,a9) ) by A98, AFF_1:15, AFF_1:def_2;
Line (b,a) // Line (b9,a9) by A19, A38, A71, AFF_1:37;
then ( a in Line (b,a) & a9 in Line (b,a) ) by A96, A99, AFF_1:15, AFF_1:45;
then b in A by A8, A9, A14, A79, A97, AFF_1:18;
hence contradiction by A2, A3, A6, A10, A14, A15, A17, AFF_1:18; ::_thesis: verum
end;
( b9 = o implies b,c // b9,c9 )
proof
assume A100: b9 = o ; ::_thesis: b,c // b9,c9
( LIN o,a,a9 & b,a // b9,a9 ) by A2, A8, A9, A14, A19, AFF_1:4, AFF_1:21;
hence b,c // b9,c9 by A21, A28, A100, AFF_1:55; ::_thesis: verum
end;
hence b,c // b9,c9 by A28, A31, A39, A24, A46; ::_thesis: verum
end;
hence b,c // b9,c9 by A10, A11, A12, A13, A15, AFF_1:51; ::_thesis: verum
end;
theorem :: AFF_3:7
for AP being AffinPlane st AP is satisfying_DES2_1 holds
AP is satisfying_DES2
proof
let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES2_1 implies AP is satisfying_DES2 )
assume A1: AP is satisfying_DES2_1 ; ::_thesis: AP is satisfying_DES2
let A be Subset of AP; :: according to AFF_3:def_5 ::_thesis: for P, C being Subset of AP
for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q
let P, C be Subset of AP; ::_thesis: for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q
let a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 implies a,c // p,q )
assume that
A2: A is being_line and
A3: P is being_line and
A4: C is being_line and
A5: A <> P and
A6: A <> C and
A7: P <> C and
A8: a in A and
A9: a9 in A and
A10: b in P and
A11: b9 in P and
A12: c in C and
A13: c9 in C and
A14: A // P and
A15: A // C and
A16: not LIN b,a,c and
A17: not LIN b9,a9,c9 and
A18: p <> q and
A19: a <> a9 and
A20: LIN b,a,p and
A21: LIN b9,a9,p and
A22: ( LIN b,c,q & LIN b9,c9,q ) and
A23: a,c // a9,c9 ; ::_thesis: a,c // p,q
A24: P // C by A14, A15, AFF_1:44;
set P9 = Line (b9,a9);
A25: p in Line (b9,a9) by A21, AFF_1:def_2;
a9 <> b9 by A17, AFF_1:7;
then A26: Line (b9,a9) is being_line by AFF_1:def_3;
set K = Line (a,c);
set N = Line (a9,c9);
set D = Line (b,c);
set T = Line (b9,c9);
A27: ( q in Line (b,c) & q in Line (b9,c9) ) by A22, AFF_1:def_2;
A28: c9 in Line (a9,c9) by AFF_1:15;
b <> c by A16, AFF_1:7;
then A29: Line (b,c) is being_line by AFF_1:def_3;
b9 <> c9 by A17, AFF_1:7;
then A30: Line (b9,c9) is being_line by AFF_1:def_3;
A31: a <> c by A16, AFF_1:7;
then A32: Line (a,c) is being_line by AFF_1:def_3;
A33: a9 <> c9 by A17, AFF_1:7;
then A34: Line (a9,c9) is being_line by AFF_1:def_3;
then consider M being Subset of AP such that
A35: p in M and
A36: Line (a9,c9) // M by AFF_1:49;
A37: Line (a,c) // Line (a9,c9) by A23, A31, A33, AFF_1:37;
then A38: Line (a,c) // M by A36, AFF_1:44;
A39: c in Line (b,c) by AFF_1:15;
A40: b in Line (b,c) by AFF_1:15;
set A9 = Line (b,a);
A41: p in Line (b,a) by A20, AFF_1:def_2;
a <> b by A16, AFF_1:7;
then A42: Line (b,a) is being_line by AFF_1:def_3;
A43: c9 in Line (b9,c9) by AFF_1:15;
A44: b9 in Line (b9,c9) by AFF_1:15;
A45: a9 in Line (a9,c9) by AFF_1:15;
A46: a in Line (a,c) by AFF_1:15;
A47: a9 in Line (b9,a9) by AFF_1:15;
A48: b9 in Line (b9,a9) by AFF_1:15;
A49: a in Line (b,a) by AFF_1:15;
A50: b in Line (b,a) by AFF_1:15;
A51: c in Line (a,c) by AFF_1:15;
then A52: Line (a,c) <> A by A6, A12, A15, AFF_1:45;
A53: c <> c9
proof
assume c = c9 ; ::_thesis: contradiction
then Line (a,c) = Line (a9,c9) by A51, A28, A37, AFF_1:45;
hence contradiction by A2, A8, A9, A19, A32, A46, A45, A52, AFF_1:18; ::_thesis: verum
end;
A54: Line (b,c) <> Line (b9,c9)
proof
assume Line (b,c) = Line (b9,c9) ; ::_thesis: contradiction
then Line (b,c) = C by A4, A12, A13, A29, A39, A43, A53, AFF_1:18;
hence contradiction by A7, A10, A24, A40, AFF_1:45; ::_thesis: verum
end;
A55: b <> b9
proof
A56: Line (b,a) <> Line (b9,a9)
proof
assume Line (b,a) = Line (b9,a9) ; ::_thesis: contradiction
then Line (b,a) = A by A2, A8, A9, A19, A42, A49, A47, AFF_1:18;
hence contradiction by A5, A10, A14, A50, AFF_1:45; ::_thesis: verum
end;
assume A57: b = b9 ; ::_thesis: contradiction
then b9 = q by A29, A30, A40, A44, A27, A54, AFF_1:18;
hence contradiction by A18, A42, A26, A50, A41, A48, A25, A57, A56, AFF_1:18; ::_thesis: verum
end;
A58: M is being_line by A36, AFF_1:36;
A59: now__::_thesis:_(_not_Line_(b9,c9)_//_M_implies_a,c_//_p,q_)
assume not Line (b9,c9) // M ; ::_thesis: a,c // p,q
then consider x being Element of AP such that
A60: x in Line (b9,c9) and
A61: x in M by A30, A58, AFF_1:58;
A62: p <> x
proof
assume p = x ; ::_thesis: contradiction
then ( p = b9 or Line (b9,c9) = Line (b9,a9) ) by A30, A44, A26, A48, A25, A60, AFF_1:18;
then ( LIN b,b9,a or c9 in Line (b9,a9) ) by A42, A50, A49, A41, AFF_1:15, AFF_1:21;
then a in P by A3, A10, A11, A17, A55, AFF_1:25, AFF_1:def_2;
hence contradiction by A5, A8, A14, AFF_1:45; ::_thesis: verum
end;
not b,x // C
proof
assume A63: b,x // C ; ::_thesis: contradiction
C // P by A14, A15, AFF_1:44;
then b,x // P by A63, AFF_1:43;
then x in P by A3, A10, AFF_1:23;
then ( b9 in M or c9 in P ) by A3, A11, A30, A44, A43, A60, A61, AFF_1:18;
then ( b9 = p or M = Line (b9,a9) ) by A7, A13, A24, A26, A48, A25, A35, A58, AFF_1:18, AFF_1:45;
then ( LIN b,b9,a or Line (a9,c9) // Line (b9,a9) ) by A20, A36, AFF_1:6;
then ( a in P or Line (a9,c9) = Line (b9,a9) ) by A3, A10, A11, A45, A47, A55, AFF_1:25, AFF_1:45;
hence contradiction by A5, A8, A14, A17, A28, AFF_1:45, AFF_1:def_2; ::_thesis: verum
end;
then consider y being Element of AP such that
A64: y in C and
A65: LIN b,x,y by A4, AFF_1:59;
A66: LIN b,y,x by A65, AFF_1:6;
A67: not LIN b,a,y
proof
A68: now__::_thesis:_not_x_=_p
assume x = p ; ::_thesis: contradiction
then ( p = b9 or Line (b9,c9) = Line (b9,a9) ) by A30, A44, A26, A48, A25, A60, AFF_1:18;
then ( LIN b,b9,a or c9 in Line (b9,a9) ) by A42, A50, A49, A41, AFF_1:15, AFF_1:21;
then a in P by A3, A10, A11, A17, A55, AFF_1:25, AFF_1:def_2;
hence contradiction by A5, A8, A14, AFF_1:45; ::_thesis: verum
end;
assume LIN b,a,y ; ::_thesis: contradiction
then A69: LIN b,y,a by AFF_1:6;
LIN b,y,b by AFF_1:7;
then ( b = y or LIN a,b,x ) by A66, A69, AFF_1:8;
then x in Line (b,a) by A7, A10, A24, A64, AFF_1:45, AFF_1:def_2;
then ( x = p or Line (b,a) = M ) by A42, A41, A35, A58, A61, AFF_1:18;
then Line (a,c) = Line (b,a) by A46, A49, A38, A68, AFF_1:45;
hence contradiction by A16, A51, AFF_1:def_2; ::_thesis: verum
end;
( LIN b9,c9,x & a9,c9 // p,x ) by A30, A45, A28, A44, A43, A35, A36, A60, A61, AFF_1:21, AFF_1:39;
then a9,c9 // a,y by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A13, A14, A15, A17, A20, A21, A64, A66, A67, A62, Def6;
then a,c // a,y by A23, A33, AFF_1:5;
then LIN a,c,y by AFF_1:def_1;
then y in Line (a,c) by AFF_1:def_2;
then ( Line (a,c) = C or y = c ) by A4, A12, A32, A51, A64, AFF_1:18;
then ( a in C or LIN b,c,x ) by A65, AFF_1:6, AFF_1:15;
then x in Line (b,c) by A6, A8, A15, AFF_1:45, AFF_1:def_2;
then ( q in M or c9 in Line (b,c) ) by A29, A30, A43, A27, A60, A61, AFF_1:18;
then ( a,c // p,q or LIN c,c9,b ) by A29, A46, A51, A40, A39, A35, A38, AFF_1:21, AFF_1:39;
then ( a,c // p,q or b in C ) by A4, A12, A13, A53, AFF_1:25;
hence a,c // p,q by A7, A10, A24, AFF_1:45; ::_thesis: verum
end;
A70: now__::_thesis:_(_not_M_//_Line_(b,c)_implies_a,c_//_p,q_)
assume not M // Line (b,c) ; ::_thesis: a,c // p,q
then consider x being Element of AP such that
A71: x in M and
A72: x in Line (b,c) by A29, A58, AFF_1:58;
A73: p <> x
proof
assume p = x ; ::_thesis: contradiction
then ( p = b or Line (b,c) = Line (b,a) ) by A29, A40, A42, A50, A41, A72, AFF_1:18;
then ( LIN b,b9,a9 or c in Line (b,a) ) by A26, A48, A47, A25, AFF_1:15, AFF_1:21;
then a9 in P by A3, A10, A11, A16, A55, AFF_1:25, AFF_1:def_2;
hence contradiction by A5, A9, A14, AFF_1:45; ::_thesis: verum
end;
not b9,x // C
proof
A74: now__::_thesis:_not_b_=_p
assume b = p ; ::_thesis: contradiction
then LIN b,b9,a9 by A26, A48, A47, A25, AFF_1:21;
then a9 in P by A3, A10, A11, A55, AFF_1:25;
hence contradiction by A5, A9, A14, AFF_1:45; ::_thesis: verum
end;
assume A75: b9,x // C ; ::_thesis: contradiction
C // P by A14, A15, AFF_1:44;
then b9,x // P by A75, AFF_1:43;
then x in P by A3, A11, AFF_1:23;
then ( x = b or Line (b,c) = P ) by A3, A10, A29, A40, A72, AFF_1:18;
then ( b = p or M = Line (b,a) ) by A7, A12, A24, A39, A42, A50, A41, A35, A58, A71, AFF_1:18, AFF_1:45;
then b in Line (a,c) by A46, A50, A49, A38, A74, AFF_1:45;
hence contradiction by A16, A32, A46, A51, AFF_1:21; ::_thesis: verum
end;
then consider y being Element of AP such that
A76: y in C and
A77: LIN b9,x,y by A4, AFF_1:59;
A78: LIN b9,y,x by A77, AFF_1:6;
A79: not LIN b9,a9,y
proof
A80: now__::_thesis:_not_x_=_p
assume x = p ; ::_thesis: contradiction
then ( p = b or Line (b,c) = Line (b,a) ) by A29, A40, A42, A50, A41, A72, AFF_1:18;
then ( LIN b,b9,a9 or c in Line (b,a) ) by A26, A48, A47, A25, AFF_1:15, AFF_1:21;
then a9 in P by A3, A10, A11, A16, A55, AFF_1:25, AFF_1:def_2;
hence contradiction by A5, A9, A14, AFF_1:45; ::_thesis: verum
end;
assume LIN b9,a9,y ; ::_thesis: contradiction
then A81: LIN b9,y,a9 by AFF_1:6;
LIN b9,y,b9 by AFF_1:7;
then ( b9 = y or LIN a9,b9,x ) by A78, A81, AFF_1:8;
then x in Line (b9,a9) by A7, A11, A24, A76, AFF_1:45, AFF_1:def_2;
then ( x = p or Line (b9,a9) = M ) by A26, A25, A35, A58, A71, AFF_1:18;
then Line (a9,c9) = Line (b9,a9) by A45, A47, A36, A80, AFF_1:45;
hence contradiction by A17, A28, AFF_1:def_2; ::_thesis: verum
end;
( LIN b,c,x & a,c // p,x ) by A29, A46, A51, A40, A39, A35, A38, A71, A72, AFF_1:21, AFF_1:39;
then a,c // a9,y by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A14, A15, A16, A20, A21, A76, A78, A79, A73, Def6;
then a9,y // a9,c9 by A23, A31, AFF_1:5;
then LIN a9,y,c9 by AFF_1:def_1;
then LIN a9,c9,y by AFF_1:6;
then y in Line (a9,c9) by AFF_1:def_2;
then ( Line (a9,c9) = C or y = c9 ) by A4, A13, A34, A28, A76, AFF_1:18;
then ( a9 in C or LIN b9,c9,x ) by A77, AFF_1:6, AFF_1:15;
then x in Line (b9,c9) by A6, A9, A15, AFF_1:45, AFF_1:def_2;
then ( q in M or c9 in Line (b,c) ) by A29, A30, A43, A27, A71, A72, AFF_1:18;
then ( a,c // p,q or LIN c,c9,b ) by A29, A46, A51, A40, A39, A35, A38, AFF_1:21, AFF_1:39;
then ( a,c // p,q or b in C ) by A4, A12, A13, A53, AFF_1:25;
hence a,c // p,q by A7, A10, A24, AFF_1:45; ::_thesis: verum
end;
( not M // Line (b,c) or not Line (b9,c9) // M )
proof
assume ( M // Line (b,c) & Line (b9,c9) // M ) ; ::_thesis: contradiction
then Line (b9,c9) // Line (b,c) by AFF_1:44;
hence contradiction by A27, A54, AFF_1:45; ::_thesis: verum
end;
hence a,c // p,q by A70, A59; ::_thesis: verum
end;
theorem :: AFF_3:8
for AP being AffinPlane holds
( AP is satisfying_DES2_1 iff AP is satisfying_DES2_3 )
proof
let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES2_1 iff AP is satisfying_DES2_3 )
A1: ( AP is satisfying_DES2_1 implies AP is satisfying_DES2_3 )
proof
assume A2: AP is satisfying_DES2_1 ; ::_thesis: AP is satisfying_DES2_3
thus AP is satisfying_DES2_3 ::_thesis: verum
proof
let A be Subset of AP; :: according to AFF_3:def_8 ::_thesis: for P, C being Subset of AP
for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
A // C
let P, C be Subset of AP; ::_thesis: for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
A // C
let a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q implies A // C )
assume that
A3: A is being_line and
A4: P is being_line and
A5: C is being_line and
A6: A <> P and
A7: A <> C and
A8: P <> C and
A9: a in A and
A10: a9 in A and
A11: b in P and
A12: b9 in P and
A13: c in C and
A14: c9 in C and
A15: A // P and
A16: not LIN b,a,c and
A17: not LIN b9,a9,c9 and
A18: p <> q and
A19: c <> c9 and
A20: LIN b,a,p and
A21: LIN b9,a9,p and
A22: LIN b,c,q and
A23: LIN b9,c9,q and
A24: a,c // a9,c9 and
A25: a,c // p,q ; ::_thesis: A // C
now__::_thesis:_A_//_C
set A9 = Line (a,c);
set P9 = Line (p,q);
set C9 = Line (a9,c9);
A26: LIN p,a9,b9 by A21, AFF_1:6;
A27: a <> c by A16, AFF_1:7;
then A28: ( Line (a,c) is being_line & a in Line (a,c) ) by AFF_1:24;
A29: q <> c
proof
assume A30: q = c ; ::_thesis: contradiction
then c,p // c,a by A25, AFF_1:4;
then LIN c,p,a by AFF_1:def_1;
then A31: LIN p,a,c by AFF_1:6;
( LIN p,a,b & LIN p,a,a ) by A20, AFF_1:6, AFF_1:7;
then a = p by A16, A31, AFF_1:8;
then LIN a,a9,b9 by A21, AFF_1:6;
then ( b9 in A or a = a9 ) by A3, A9, A10, AFF_1:25;
then a9,c9 // a9,c by A6, A12, A15, A24, AFF_1:4, AFF_1:45;
then LIN a9,c9,c by AFF_1:def_1;
then LIN c,c9,a9 by AFF_1:6;
then A32: a9 in C by A5, A13, A14, A19, AFF_1:25;
LIN c,c9,b9 by A23, A30, AFF_1:6;
then b9 in C by A5, A13, A14, A19, AFF_1:25;
hence contradiction by A5, A14, A17, A32, AFF_1:21; ::_thesis: verum
end;
A33: a <> p
proof
assume a = p ; ::_thesis: contradiction
then LIN a,c,q by A25, AFF_1:def_1;
then A34: LIN c,q,a by AFF_1:6;
( LIN c,q,b & LIN c,q,c ) by A22, AFF_1:6, AFF_1:7;
hence contradiction by A16, A29, A34, AFF_1:8; ::_thesis: verum
end;
A35: a <> a9
proof
A36: ( LIN p,a,b & LIN p,a,a ) by A20, AFF_1:6, AFF_1:7;
assume A37: a = a9 ; ::_thesis: contradiction
then LIN a,c,c9 by A24, AFF_1:def_1;
then LIN c,c9,a by AFF_1:6;
then A38: a in C by A5, A13, A14, A19, AFF_1:25;
LIN p,a,b9 by A21, A37, AFF_1:6;
then ( b = b9 or a in P ) by A4, A11, A12, A33, A36, AFF_1:8, AFF_1:25;
then A39: LIN q,b,c9 by A6, A9, A15, A23, AFF_1:6, AFF_1:45;
( LIN q,b,c & LIN q,b,b ) by A22, AFF_1:6, AFF_1:7;
then A40: ( q = b or LIN c,c9,b ) by A39, AFF_1:8;
not b in C by A5, A13, A16, A38, AFF_1:21;
then LIN p,q,a by A5, A13, A14, A19, A20, A40, AFF_1:6, AFF_1:25;
then p,q // p,a by AFF_1:def_1;
then a,c // p,a by A18, A25, AFF_1:5;
then a,c // a,p by AFF_1:4;
then LIN a,c,p by AFF_1:def_1;
then A41: p in C by A5, A13, A27, A38, AFF_1:25;
LIN p,a,b by A20, AFF_1:6;
then b in C by A5, A33, A38, A41, AFF_1:25;
hence contradiction by A5, A13, A16, A38, AFF_1:21; ::_thesis: verum
end;
A42: b <> b9
proof
A43: p,q // c,a by A25, AFF_1:4;
A44: ( LIN q,b,c & LIN q,b,b ) by A22, AFF_1:6, AFF_1:7;
A45: ( LIN p,b,a & LIN p,b,b ) by A20, AFF_1:6, AFF_1:7;
assume A46: b = b9 ; ::_thesis: contradiction
then LIN p,b,a9 by A21, AFF_1:6;
then A47: ( p = b or b in A ) by A3, A9, A10, A35, A45, AFF_1:8, AFF_1:25;
LIN q,b,c9 by A23, A46, AFF_1:6;
then ( b = q or LIN c,c9,b ) by A44, AFF_1:8;
then A48: b in C by A5, A6, A11, A13, A14, A15, A18, A19, A47, AFF_1:25, AFF_1:45;
then q in C by A5, A6, A11, A13, A15, A16, A20, A22, A47, AFF_1:25, AFF_1:45;
then a in C by A5, A6, A11, A13, A15, A18, A47, A48, A43, AFF_1:45, AFF_1:48;
hence contradiction by A5, A13, A16, A48, AFF_1:21; ::_thesis: verum
end;
then A49: a9,a // b9,b by A3, A4, A9, A10, A11, A12, A15, A35, AFF_1:38;
A50: a9 <> c9 by A17, AFF_1:7;
then A51: Line (a9,c9) is being_line by AFF_1:24;
A52: c9 in Line (a9,c9) by A50, AFF_1:24;
A53: LIN p,a,b by A20, AFF_1:6;
A54: not LIN p,a9,a
proof
assume LIN p,a9,a ; ::_thesis: contradiction
then A55: LIN p,a,a9 by AFF_1:6;
LIN p,a,a by AFF_1:7;
then b in A by A3, A9, A10, A33, A35, A53, A55, AFF_1:8, AFF_1:25;
hence contradiction by A6, A11, A15, AFF_1:45; ::_thesis: verum
end;
A56: LIN q,c9,b9 by A23, AFF_1:6;
A57: a9 in Line (a9,c9) by A50, AFF_1:24;
A58: c in Line (a,c) by A27, AFF_1:24;
then A59: Line (a9,c9) // Line (a,c) by A24, A27, A50, A51, A28, A57, A52, AFF_1:38;
A60: Line (a,c) <> Line (a9,c9)
proof
assume A61: Line (a,c) = Line (a9,c9) ; ::_thesis: contradiction
then LIN a,a9,c9 by A28, A57, A52, AFF_1:21;
then A62: c9 in A by A3, A9, A10, A35, AFF_1:25;
LIN a,a9,c by A28, A58, A57, A61, AFF_1:21;
then c in A by A3, A9, A10, A35, AFF_1:25;
hence contradiction by A3, A5, A7, A13, A14, A19, A62, AFF_1:18; ::_thesis: verum
end;
A63: LIN q,c,b by A22, AFF_1:6;
A64: p in Line (p,q) by A18, AFF_1:24;
A65: Line (a,c) <> Line (p,q)
proof
assume Line (a,c) = Line (p,q) ; ::_thesis: contradiction
then A66: ( LIN p,a,c & LIN p,a,a ) by A28, A58, A64, AFF_1:21;
LIN p,a,b by A20, AFF_1:6;
hence contradiction by A16, A33, A66, AFF_1:8; ::_thesis: verum
end;
A67: Line (p,q) is being_line by A18, AFF_1:24;
A68: Line (p,q) <> Line (a9,c9)
proof
assume Line (p,q) = Line (a9,c9) ; ::_thesis: contradiction
then A69: ( LIN p,a9,c9 & LIN p,a9,a9 ) by A67, A64, A57, A52, AFF_1:21;
LIN p,a9,b9 by A21, AFF_1:6;
then p = a9 by A17, A69, AFF_1:8;
then LIN a,a9,b by A20, AFF_1:6;
then b in A by A3, A9, A10, A35, AFF_1:25;
hence contradiction by A6, A11, A15, AFF_1:45; ::_thesis: verum
end;
A70: a9,c9 // p,q by A24, A25, A27, AFF_1:5;
A71: not LIN q,c9,c
proof
A72: now__::_thesis:_not_q_=_c9
assume q = c9 ; ::_thesis: contradiction
then c9,a9 // c9,p by A70, AFF_1:4;
then LIN c9,a9,p by AFF_1:def_1;
then p in Line (a9,c9) by A50, A51, A57, A52, AFF_1:25;
then ( p = a9 or b9 in Line (a9,c9) ) by A51, A57, A26, AFF_1:25;
then LIN a,a9,b by A17, A20, A51, A57, A52, AFF_1:6, AFF_1:21;
then b in A by A3, A9, A10, A35, AFF_1:25;
hence contradiction by A6, A11, A15, AFF_1:45; ::_thesis: verum
end;
assume A73: LIN q,c9,c ; ::_thesis: contradiction
LIN q,c9,c9 by AFF_1:7;
then A74: b9 in C by A5, A13, A14, A19, A56, A73, A72, AFF_1:8, AFF_1:25;
A75: LIN q,c,c by AFF_1:7;
LIN q,c,c9 by A73, AFF_1:6;
then b in C by A5, A13, A14, A19, A29, A63, A75, AFF_1:8, AFF_1:25;
hence contradiction by A4, A5, A8, A11, A12, A42, A74, AFF_1:18; ::_thesis: verum
end;
A76: q in Line (p,q) by A18, AFF_1:24;
then Line (a9,c9) // Line (p,q) by A18, A50, A67, A51, A64, A57, A52, A70, AFF_1:38;
then a9,a // c9,c by A2, A67, A51, A28, A58, A64, A76, A57, A52, A42, A65, A60, A68, A59, A49, A53, A26, A63, A56, A54, A71, Def6;
hence A // C by A3, A5, A9, A10, A13, A14, A19, A35, AFF_1:38; ::_thesis: verum
end;
hence A // C ; ::_thesis: verum
end;
end;
( AP is satisfying_DES2_3 implies AP is satisfying_DES2_1 )
proof
assume A77: AP is satisfying_DES2_3 ; ::_thesis: AP is satisfying_DES2_1
thus AP is satisfying_DES2_1 ::_thesis: verum
proof
let A be Subset of AP; :: according to AFF_3:def_6 ::_thesis: for P, C being Subset of AP
for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9
let P, C be Subset of AP; ::_thesis: for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9
let a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q implies a,c // a9,c9 )
assume that
A78: A is being_line and
A79: P is being_line and
A80: C is being_line and
A81: A <> P and
A <> C and
A82: P <> C and
A83: a in A and
A84: a9 in A and
A85: b in P and
A86: b9 in P and
A87: c in C and
A88: c9 in C and
A89: A // P and
A90: A // C and
A91: not LIN b,a,c and
A92: not LIN b9,a9,c9 and
A93: p <> q and
A94: LIN b,a,p and
A95: LIN b9,a9,p and
A96: LIN b,c,q and
A97: LIN b9,c9,q and
A98: a,c // p,q ; ::_thesis: a,c // a9,c9
A99: C // P by A89, A90, AFF_1:44;
then A100: c,c9 // b,b9 by A85, A86, A87, A88, AFF_1:39;
assume A101: not a,c // a9,c9 ; ::_thesis: contradiction
A102: q <> c
proof
assume A103: q = c ; ::_thesis: contradiction
then c,p // c,a by A98, AFF_1:4;
then LIN c,p,a by AFF_1:def_1;
then A104: LIN p,a,c by AFF_1:6;
( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:6, AFF_1:7;
then a = p by A91, A104, AFF_1:8;
then LIN a,a9,b9 by A95, AFF_1:6;
then A105: ( b9 in A or a = a9 ) by A78, A83, A84, AFF_1:25;
LIN c,c9,b9 by A97, A103, AFF_1:6;
then ( c = c9 or b9 in C ) by A80, A87, A88, AFF_1:25;
hence contradiction by A81, A82, A86, A89, A101, A99, A105, AFF_1:2, AFF_1:45; ::_thesis: verum
end;
A106: a <> p
proof
assume a = p ; ::_thesis: contradiction
then LIN a,c,q by A98, AFF_1:def_1;
then A107: LIN c,q,a by AFF_1:6;
( LIN c,q,b & LIN c,q,c ) by A96, AFF_1:6, AFF_1:7;
hence contradiction by A91, A102, A107, AFF_1:8; ::_thesis: verum
end;
A108: a <> a9
proof
A109: ( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:6, AFF_1:7;
assume A110: a = a9 ; ::_thesis: contradiction
then LIN p,a,b9 by A95, AFF_1:6;
then ( a in P or b = b9 ) by A79, A85, A86, A106, A109, AFF_1:8, AFF_1:25;
then A111: LIN b,q,c9 by A81, A83, A89, A97, AFF_1:6, AFF_1:45;
( LIN b,q,c & LIN b,q,b ) by A96, AFF_1:6, AFF_1:7;
then ( b = q or c = c9 or b in C ) by A80, A87, A88, A111, AFF_1:8, AFF_1:25;
then LIN p,q,a by A82, A85, A94, A101, A99, A110, AFF_1:2, AFF_1:6, AFF_1:45;
then p,q // p,a by AFF_1:def_1;
then a,c // p,a by A93, A98, AFF_1:5;
then a,c // a,p by AFF_1:4;
then LIN a,c,p by AFF_1:def_1;
then A112: LIN p,a,c by AFF_1:6;
( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:6, AFF_1:7;
hence contradiction by A91, A106, A112, AFF_1:8; ::_thesis: verum
end;
A113: not LIN p,a,a9
proof
assume A114: LIN p,a,a9 ; ::_thesis: contradiction
( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:6, AFF_1:7;
then b in A by A78, A83, A84, A106, A108, A114, AFF_1:8, AFF_1:25;
hence contradiction by A81, A85, A89, AFF_1:45; ::_thesis: verum
end;
set A9 = Line (a,c);
set P9 = Line (p,q);
set C9 = Line (a9,c9);
A115: a <> c by A91, AFF_1:7;
then A116: Line (a,c) is being_line by AFF_1:24;
A117: ( c,c9 // a,a9 & LIN q,c,b ) by A83, A84, A87, A88, A90, A96, AFF_1:6, AFF_1:39;
A118: LIN p,a9,b9 by A95, AFF_1:6;
A119: ( a in Line (a,c) & c in Line (a,c) ) by A115, AFF_1:24;
A120: b <> b9
proof
assume b = b9 ; ::_thesis: contradiction
then A121: LIN b,p,a9 by A95, AFF_1:6;
( LIN b,p,a & LIN b,p,b ) by A94, AFF_1:6, AFF_1:7;
then A122: ( b = p or b in A ) by A78, A83, A84, A108, A121, AFF_1:8, AFF_1:25;
then LIN p,q,c by A81, A85, A89, A96, AFF_1:6, AFF_1:45;
then p,q // p,c by AFF_1:def_1;
then a,c // p,c by A93, A98, AFF_1:5;
then c,a // c,p by AFF_1:4;
then LIN c,a,p by AFF_1:def_1;
hence contradiction by A81, A85, A89, A91, A122, AFF_1:6, AFF_1:45; ::_thesis: verum
end;
A123: not LIN q,c,c9
proof
assume A124: LIN q,c,c9 ; ::_thesis: contradiction
( LIN q,c,b & LIN q,c,c ) by A96, AFF_1:6, AFF_1:7;
then ( c = c9 or b in C ) by A80, A87, A88, A102, A124, AFF_1:8, AFF_1:25;
then A125: LIN q,c,b9 by A82, A85, A97, A99, AFF_1:6, AFF_1:45;
( LIN q,c,b & LIN q,c,c ) by A96, AFF_1:6, AFF_1:7;
then c in P by A79, A85, A86, A102, A120, A125, AFF_1:8, AFF_1:25;
hence contradiction by A82, A87, A99, AFF_1:45; ::_thesis: verum
end;
A126: ( LIN q,c9,b9 & LIN p,a,b ) by A94, A97, AFF_1:6;
A127: a9 <> c9 by A92, AFF_1:7;
then A128: Line (a9,c9) is being_line by AFF_1:24;
A129: p in Line (p,q) by A93, AFF_1:24;
A130: Line (a,c) <> Line (p,q)
proof
assume Line (a,c) = Line (p,q) ; ::_thesis: contradiction
then A131: ( LIN p,a,c & LIN p,a,a ) by A116, A119, A129, AFF_1:21;
LIN p,a,b by A94, AFF_1:6;
hence contradiction by A91, A106, A131, AFF_1:8; ::_thesis: verum
end;
A132: ( Line (p,q) is being_line & q in Line (p,q) ) by A93, AFF_1:24;
then A133: Line (a,c) // Line (p,q) by A93, A98, A115, A116, A119, A129, AFF_1:38;
A134: ( a9 in Line (a9,c9) & c9 in Line (a9,c9) ) by A127, AFF_1:24;
then Line (a,c) <> Line (a9,c9) by A101, A116, A119, AFF_1:51;
then Line (a,c) // Line (a9,c9) by A77, A127, A116, A128, A119, A129, A132, A134, A100, A133, A130, A120, A123, A113, A117, A126, A118, Def8;
hence contradiction by A101, A119, A134, AFF_1:39; ::_thesis: verum
end;
end;
hence ( AP is satisfying_DES2_1 iff AP is satisfying_DES2_3 ) by A1; ::_thesis: verum
end;
theorem :: AFF_3:9
for AP being AffinPlane holds
( AP is satisfying_DES2 iff AP is satisfying_DES2_2 )
proof
let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES2 iff AP is satisfying_DES2_2 )
A1: ( AP is satisfying_DES2 implies AP is satisfying_DES2_2 )
proof
assume A2: AP is satisfying_DES2 ; ::_thesis: AP is satisfying_DES2_2
thus AP is satisfying_DES2_2 ::_thesis: verum
proof
let A be Subset of AP; :: according to AFF_3:def_7 ::_thesis: for P, C being Subset of AP
for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
A // P
let P, C be Subset of AP; ::_thesis: for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds
A // P
let a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q implies A // P )
assume that
A3: A is being_line and
A4: P is being_line and
A5: C is being_line and
A6: A <> P and
A7: A <> C and
A8: P <> C and
A9: ( a in A & a9 in A ) and
A10: ( b in P & b9 in P ) and
A11: c in C and
A12: c9 in C and
A13: A // C and
A14: not LIN b,a,c and
A15: not LIN b9,a9,c9 and
A16: p <> q and
A17: a <> a9 and
A18: LIN b,a,p and
A19: LIN b9,a9,p and
A20: LIN b,c,q and
A21: LIN b9,c9,q and
A22: a,c // a9,c9 and
A23: a,c // p,q ; ::_thesis: A // P
A24: LIN q,c9,b9 by A21, AFF_1:6;
A25: c <> c9
proof
assume c = c9 ; ::_thesis: contradiction
then c,a // c,a9 by A22, AFF_1:4;
then LIN c,a,a9 by AFF_1:def_1;
then LIN a,a9,c by AFF_1:6;
then c in A by A3, A9, A17, AFF_1:25;
hence contradiction by A7, A11, A13, AFF_1:45; ::_thesis: verum
end;
A26: b <> b9
proof
A27: now__::_thesis:_(_b_=_p_implies_not_b_in_C_)
assume that
A28: b = p and
b in C ; ::_thesis: contradiction
LIN p,q,c by A20, A28, AFF_1:6;
then p,q // p,c by AFF_1:def_1;
then a,c // p,c by A16, A23, AFF_1:5;
then c,a // c,p by AFF_1:4;
then LIN c,a,p by AFF_1:def_1;
hence contradiction by A14, A28, AFF_1:6; ::_thesis: verum
end;
A29: ( LIN b,p,a & LIN b,p,b ) by A18, AFF_1:6, AFF_1:7;
assume A30: b = b9 ; ::_thesis: contradiction
then LIN b,p,a9 by A19, AFF_1:6;
then A31: ( b = p or b in A ) by A3, A9, A17, A29, AFF_1:8, AFF_1:25;
A32: ( LIN b,q,c & LIN b,q,b ) by A20, AFF_1:6, AFF_1:7;
LIN b,q,c9 by A21, A30, AFF_1:6;
then A33: ( b = q or b in C ) by A5, A11, A12, A25, A32, AFF_1:8, AFF_1:25;
then LIN q,p,a by A7, A13, A18, A31, A27, AFF_1:6, AFF_1:45;
then q,p // q,a by AFF_1:def_1;
then p,q // q,a by AFF_1:4;
then a,c // q,a by A16, A23, AFF_1:5;
then a,c // a,q by AFF_1:4;
then LIN a,c,q by AFF_1:def_1;
hence contradiction by A7, A13, A14, A31, A33, A27, AFF_1:6, AFF_1:45; ::_thesis: verum
end;
A34: a <> p
proof
assume A35: a = p ; ::_thesis: contradiction
then LIN a,c,q by A23, AFF_1:def_1;
then A36: LIN c,q,a by AFF_1:6;
( LIN c,q,b & LIN c,q,c ) by A20, AFF_1:6, AFF_1:7;
then q = c by A14, A36, AFF_1:8;
then LIN c,c9,b9 by A21, AFF_1:6;
then A37: ( c = c9 or b9 in C ) by A5, A11, A12, AFF_1:25;
LIN a,a9,b9 by A19, A35, AFF_1:6;
then b9 in A by A3, A9, A17, AFF_1:25;
then c,a // c,a9 by A7, A13, A22, A37, AFF_1:4, AFF_1:45;
then LIN c,a,a9 by AFF_1:def_1;
then LIN a,a9,c by AFF_1:6;
then c in A by A3, A9, A17, AFF_1:25;
hence contradiction by A7, A11, A13, AFF_1:45; ::_thesis: verum
end;
A38: q <> c
proof
assume q = c ; ::_thesis: contradiction
then c,p // c,a by A23, AFF_1:4;
then LIN c,p,a by AFF_1:def_1;
then A39: LIN p,a,c by AFF_1:6;
( LIN p,a,b & LIN p,a,a ) by A18, AFF_1:6, AFF_1:7;
hence contradiction by A14, A34, A39, AFF_1:8; ::_thesis: verum
end;
A40: LIN q,c,b by A20, AFF_1:6;
set A9 = Line (a,c);
set P9 = Line (p,q);
set C9 = Line (a9,c9);
A41: a <> c by A14, AFF_1:7;
then A42: c in Line (a,c) by AFF_1:24;
A43: a9 <> p
proof
assume A44: a9 = p ; ::_thesis: contradiction
a9,c9 // p,q by A22, A23, A41, AFF_1:5;
then LIN a9,c9,q by A44, AFF_1:def_1;
then A45: LIN c9,q,a9 by AFF_1:6;
( LIN c9,q,b9 & LIN c9,q,c9 ) by A21, AFF_1:6, AFF_1:7;
then q = c9 by A15, A45, AFF_1:8;
then LIN c,c9,b by A20, AFF_1:6;
then A46: b in C by A5, A11, A12, A25, AFF_1:25;
LIN a,a9,b by A18, A44, AFF_1:6;
then b in A by A3, A9, A17, AFF_1:25;
hence contradiction by A7, A13, A46, AFF_1:45; ::_thesis: verum
end;
A47: c9 <> q
proof
assume c9 = q ; ::_thesis: contradiction
then a9,c9 // p,c9 by A22, A23, A41, AFF_1:5;
then c9,a9 // c9,p by AFF_1:4;
then LIN c9,a9,p by AFF_1:def_1;
then A48: LIN p,a9,c9 by AFF_1:6;
( LIN p,a9,b9 & LIN p,a9,a9 ) by A19, AFF_1:6, AFF_1:7;
hence contradiction by A15, A43, A48, AFF_1:8; ::_thesis: verum
end;
A49: not LIN q,c9,c
proof
A50: LIN q,c,c by AFF_1:7;
assume A51: LIN q,c9,c ; ::_thesis: contradiction
LIN q,c9,c9 by AFF_1:7;
then A52: b9 in C by A5, A11, A12, A25, A47, A24, A51, AFF_1:8, AFF_1:25;
LIN q,c,c9 by A51, AFF_1:6;
then b in C by A5, A11, A12, A38, A25, A40, A50, AFF_1:8, AFF_1:25;
hence contradiction by A4, A5, A8, A10, A26, A52, AFF_1:18; ::_thesis: verum
end;
A53: LIN p,a,b by A18, AFF_1:6;
A54: LIN p,a9,b9 by A19, AFF_1:6;
A55: not LIN p,a9,a
proof
A56: LIN p,a,a by AFF_1:7;
assume A57: LIN p,a9,a ; ::_thesis: contradiction
LIN p,a9,a9 by AFF_1:7;
then A58: b9 in A by A3, A9, A17, A43, A54, A57, AFF_1:8, AFF_1:25;
LIN p,a,a9 by A57, AFF_1:6;
then b in A by A3, A9, A17, A34, A53, A56, AFF_1:8, AFF_1:25;
hence contradiction by A3, A4, A6, A10, A26, A58, AFF_1:18; ::_thesis: verum
end;
A59: a9,a // c9,c by A9, A11, A12, A13, AFF_1:39;
A60: q in Line (p,q) by A16, AFF_1:24;
A61: a9 <> c9 by A15, AFF_1:7;
then A62: a9 in Line (a9,c9) by AFF_1:24;
A63: ( Line (a,c) is being_line & a in Line (a,c) ) by A41, AFF_1:24;
A64: Line (a9,c9) <> Line (a,c)
proof
assume Line (a9,c9) = Line (a,c) ; ::_thesis: contradiction
then LIN a,a9,c by A63, A42, A62, AFF_1:21;
then c in A by A3, A9, A17, AFF_1:25;
hence contradiction by A7, A11, A13, AFF_1:45; ::_thesis: verum
end;
A65: p in Line (p,q) by A16, AFF_1:24;
A66: Line (p,q) <> Line (a,c)
proof
assume Line (p,q) = Line (a,c) ; ::_thesis: contradiction
then A67: ( LIN p,a,c & LIN p,a,a ) by A63, A42, A65, AFF_1:21;
LIN p,a,b by A18, AFF_1:6;
hence contradiction by A14, A34, A67, AFF_1:8; ::_thesis: verum
end;
A68: c9 in Line (a9,c9) by A61, AFF_1:24;
A69: Line (p,q) is being_line by A16, AFF_1:24;
A70: Line (a9,c9) <> Line (p,q)
proof
assume Line (a9,c9) = Line (p,q) ; ::_thesis: contradiction
then A71: ( LIN p,a9,c9 & LIN p,a9,a9 ) by A69, A65, A62, A68, AFF_1:21;
LIN p,a9,b9 by A19, AFF_1:6;
hence contradiction by A15, A43, A71, AFF_1:8; ::_thesis: verum
end;
A72: Line (a9,c9) is being_line by A61, AFF_1:24;
a9,c9 // p,q by A22, A23, A41, AFF_1:5;
then A73: Line (a9,c9) // Line (p,q) by A16, A61, A69, A72, A65, A60, A62, A68, AFF_1:38;
Line (a9,c9) // Line (a,c) by A22, A41, A61, A72, A63, A42, A62, A68, AFF_1:38;
then a9,a // b9,b by A2, A61, A26, A69, A72, A63, A42, A65, A60, A62, A68, A73, A64, A70, A66, A54, A53, A24, A40, A55, A49, A59, Def5;
hence A // P by A3, A4, A9, A10, A17, A26, AFF_1:38; ::_thesis: verum
end;
end;
( AP is satisfying_DES2_2 implies AP is satisfying_DES2 )
proof
assume A74: AP is satisfying_DES2_2 ; ::_thesis: AP is satisfying_DES2
thus AP is satisfying_DES2 ::_thesis: verum
proof
let A be Subset of AP; :: according to AFF_3:def_5 ::_thesis: for P, C being Subset of AP
for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q
let P, C be Subset of AP; ::_thesis: for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q
let a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 implies a,c // p,q )
assume that
A75: A is being_line and
P is being_line and
A76: C is being_line and
A77: A <> P and
A78: A <> C and
A79: P <> C and
A80: ( a in A & a9 in A ) and
A81: b in P and
A82: b9 in P and
A83: c in C and
A84: c9 in C and
A85: A // P and
A86: A // C and
A87: not LIN b,a,c and
A88: not LIN b9,a9,c9 and
A89: p <> q and
A90: a <> a9 and
A91: LIN b,a,p and
A92: LIN b9,a9,p and
A93: LIN b,c,q and
A94: LIN b9,c9,q and
A95: a,c // a9,c9 ; ::_thesis: a,c // p,q
A96: LIN p,a,b by A91, AFF_1:6;
set A9 = Line (a,c);
set P9 = Line (p,q);
set C9 = Line (a9,c9);
A97: q in Line (p,q) by A89, AFF_1:24;
A98: a <> p
proof
assume a = p ; ::_thesis: contradiction
then LIN a,a9,b9 by A92, AFF_1:6;
then b9 in A by A75, A80, A90, AFF_1:25;
hence contradiction by A77, A82, A85, AFF_1:45; ::_thesis: verum
end;
A99: not LIN p,a,a9
proof
A100: LIN p,a,a by AFF_1:7;
assume LIN p,a,a9 ; ::_thesis: contradiction
then b in A by A75, A80, A90, A98, A96, A100, AFF_1:8, AFF_1:25;
hence contradiction by A77, A81, A85, AFF_1:45; ::_thesis: verum
end;
A101: ( LIN q,c9,b9 & LIN p,a9,b9 ) by A92, A94, AFF_1:6;
A102: a <> c by A87, AFF_1:7;
then A103: Line (a,c) is being_line by AFF_1:24;
A104: C // P by A85, A86, AFF_1:44;
then A105: c,c9 // b,b9 by A81, A82, A83, A84, AFF_1:39;
A106: c <> c9
proof
assume c = c9 ; ::_thesis: contradiction
then c,a // c,a9 by A95, AFF_1:4;
then LIN c,a,a9 by AFF_1:def_1;
then LIN a,a9,c by AFF_1:6;
then c in A by A75, A80, A90, AFF_1:25;
hence contradiction by A78, A83, A86, AFF_1:45; ::_thesis: verum
end;
A107: b <> b9
proof
A108: ( LIN b,p,a & LIN b,p,b ) by A91, AFF_1:6, AFF_1:7;
assume A109: b = b9 ; ::_thesis: contradiction
then LIN b,p,a9 by A92, AFF_1:6;
then A110: ( b = p or b in A ) by A75, A80, A90, A108, AFF_1:8, AFF_1:25;
A111: ( LIN b,q,c & LIN b,q,b ) by A93, AFF_1:6, AFF_1:7;
LIN b,q,c9 by A94, A109, AFF_1:6;
then ( b = q or b in C ) by A76, A83, A84, A106, A111, AFF_1:8, AFF_1:25;
hence contradiction by A77, A79, A81, A85, A89, A104, A110, AFF_1:45; ::_thesis: verum
end;
A112: ( a in Line (a,c) & c in Line (a,c) ) by A102, AFF_1:24;
A113: ( Line (p,q) is being_line & c,c9 // a,a9 ) by A80, A83, A84, A86, A89, AFF_1:24, AFF_1:39;
A114: p in Line (p,q) by A89, AFF_1:24;
A115: a9 <> c9 by A88, AFF_1:7;
then A116: a9 in Line (a9,c9) by AFF_1:24;
A117: Line (a,c) <> Line (a9,c9)
proof
assume Line (a,c) = Line (a9,c9) ; ::_thesis: contradiction
then LIN a,a9,c by A103, A112, A116, AFF_1:21;
then c in A by A75, A80, A90, AFF_1:25;
hence contradiction by A78, A83, A86, AFF_1:45; ::_thesis: verum
end;
A118: q <> c
proof
assume q = c ; ::_thesis: contradiction
then LIN c,c9,b9 by A94, AFF_1:6;
then b9 in C by A76, A83, A84, A106, AFF_1:25;
hence contradiction by A79, A82, A104, AFF_1:45; ::_thesis: verum
end;
A119: Line (a,c) <> Line (p,q)
proof
assume Line (a,c) = Line (p,q) ; ::_thesis: contradiction
then A120: ( LIN c,q,a & LIN c,q,c ) by A103, A112, A97, AFF_1:21;
LIN c,q,b by A93, AFF_1:6;
hence contradiction by A87, A118, A120, AFF_1:8; ::_thesis: verum
end;
A121: LIN q,c,b by A93, AFF_1:6;
A122: not LIN q,c,c9
proof
A123: LIN q,c,c by AFF_1:7;
assume LIN q,c,c9 ; ::_thesis: contradiction
then b in C by A76, A83, A84, A106, A118, A121, A123, AFF_1:8, AFF_1:25;
hence contradiction by A79, A81, A104, AFF_1:45; ::_thesis: verum
end;
A124: ( Line (a9,c9) is being_line & c9 in Line (a9,c9) ) by A115, AFF_1:24;
then Line (a,c) // Line (a9,c9) by A95, A102, A115, A103, A112, A116, AFF_1:38;
then Line (a,c) // Line (p,q) by A74, A102, A107, A103, A112, A114, A97, A116, A124, A113, A105, A121, A96, A101, A119, A117, A122, A99, Def7;
hence a,c // p,q by A112, A114, A97, AFF_1:39; ::_thesis: verum
end;
end;
hence ( AP is satisfying_DES2 iff AP is satisfying_DES2_2 ) by A1; ::_thesis: verum
end;
theorem :: AFF_3:10
for AP being AffinPlane st AP is satisfying_DES1_3 holds
AP is satisfying_DES2_1
proof
let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES1_3 implies AP is satisfying_DES2_1 )
assume A1: AP is satisfying_DES1_3 ; ::_thesis: AP is satisfying_DES2_1
let A be Subset of AP; :: according to AFF_3:def_6 ::_thesis: for P, C being Subset of AP
for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9
let P, C be Subset of AP; ::_thesis: for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9
let a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q implies a,c // a9,c9 )
assume that
A2: A is being_line and
A3: P is being_line and
A4: C is being_line and
A5: A <> P and
A6: A <> C and
A7: P <> C and
A8: a in A and
A9: a9 in A and
A10: b in P and
A11: b9 in P and
A12: c in C and
A13: c9 in C and
A14: A // P and
A15: A // C and
A16: not LIN b,a,c and
A17: not LIN b9,a9,c9 and
A18: p <> q and
A19: LIN b,a,p and
A20: LIN b9,a9,p and
A21: LIN b,c,q and
A22: LIN b9,c9,q and
A23: a,c // p,q ; ::_thesis: a,c // a9,c9
A24: P // C by A14, A15, AFF_1:44;
set K = Line (p,q);
set M = Line (a,c);
set N = Line (a9,c9);
A25: a <> c by A16, AFF_1:7;
then A26: a in Line (a,c) by AFF_1:24;
A27: ( c,c9 // a,a9 & LIN q,c,b ) by A8, A9, A12, A13, A15, A21, AFF_1:6, AFF_1:39;
A28: LIN p,a9,b9 by A20, AFF_1:6;
C // P by A14, A15, AFF_1:44;
then A29: c,c9 // b,b9 by A10, A11, A12, A13, AFF_1:39;
A30: ( LIN q,c9,b9 & LIN p,a,b ) by A19, A22, AFF_1:6;
A31: c in Line (a,c) by A25, AFF_1:24;
assume A32: not a,c // a9,c9 ; ::_thesis: contradiction
A33: c <> q
proof
assume A34: c = q ; ::_thesis: contradiction
then c,a // c,p by A23, AFF_1:4;
then LIN c,a,p by AFF_1:def_1;
then A35: LIN p,a,c by AFF_1:6;
( LIN p,a,b & LIN p,a,a ) by A19, AFF_1:6, AFF_1:7;
then p = a by A16, A35, AFF_1:8;
then LIN a,a9,b9 by A20, AFF_1:6;
then A36: ( a = a9 or b9 in A ) by A2, A8, A9, AFF_1:25;
LIN c,c9,b9 by A22, A34, AFF_1:6;
then ( c = c9 or b9 in C ) by A4, A12, A13, AFF_1:25;
hence contradiction by A5, A7, A11, A14, A32, A24, A36, AFF_1:2, AFF_1:45; ::_thesis: verum
end;
A37: c <> c9
proof
A38: now__::_thesis:_not_p_=_b
assume A39: p = b ; ::_thesis: contradiction
LIN b,q,c by A21, AFF_1:6;
then b,q // b,c by AFF_1:def_1;
then ( a,c // b,c or b = q ) by A23, A39, AFF_1:5;
then c,a // c,b by A18, A39, AFF_1:4;
then LIN c,a,b by AFF_1:def_1;
hence contradiction by A16, AFF_1:6; ::_thesis: verum
end;
A40: ( LIN q,c,b & LIN q,c,c ) by A21, AFF_1:6, AFF_1:7;
assume A41: c = c9 ; ::_thesis: contradiction
then LIN q,c,b9 by A22, AFF_1:6;
then ( b = b9 or c in P ) by A3, A10, A11, A33, A40, AFF_1:8, AFF_1:25;
then A42: LIN p,b,a9 by A7, A12, A20, A24, AFF_1:6, AFF_1:45;
( LIN p,b,a & LIN p,b,b ) by A19, AFF_1:6, AFF_1:7;
then ( a = a9 or b in A ) by A2, A8, A9, A42, A38, AFF_1:8, AFF_1:25;
hence contradiction by A5, A10, A14, A32, A41, AFF_1:2, AFF_1:45; ::_thesis: verum
end;
A43: b <> b9
proof
assume b = b9 ; ::_thesis: contradiction
then A44: LIN q,b,c9 by A22, AFF_1:6;
( LIN q,b,c & LIN q,b,b ) by A21, AFF_1:6, AFF_1:7;
then A45: ( q = b or b in C ) by A4, A12, A13, A37, A44, AFF_1:8, AFF_1:25;
b,a // b,p by A19, AFF_1:def_1;
then a,b // p,b by AFF_1:4;
then ( a,c // a,b or p = b ) by A7, A10, A23, A24, A45, AFF_1:5, AFF_1:45;
then LIN a,c,b by A7, A10, A18, A24, A45, AFF_1:45, AFF_1:def_1;
hence contradiction by A16, AFF_1:6; ::_thesis: verum
end;
A46: not LIN q,c,c9
proof
assume A47: LIN q,c,c9 ; ::_thesis: contradiction
( LIN q,c,b & LIN q,c,c ) by A21, AFF_1:6, AFF_1:7;
then b in C by A4, A12, A13, A33, A37, A47, AFF_1:8, AFF_1:25;
hence contradiction by A7, A10, A24, AFF_1:45; ::_thesis: verum
end;
A48: a9 <> c9 by A17, AFF_1:7;
then A49: Line (a9,c9) is being_line by AFF_1:24;
A50: p <> a
proof
assume p = a ; ::_thesis: contradiction
then LIN a,c,q by A23, AFF_1:def_1;
then A51: LIN c,q,a by AFF_1:6;
( LIN c,q,b & LIN c,q,c ) by A21, AFF_1:6, AFF_1:7;
hence contradiction by A16, A33, A51, AFF_1:8; ::_thesis: verum
end;
A52: not LIN p,a,a9
proof
assume A53: LIN p,a,a9 ; ::_thesis: contradiction
( LIN p,a,b & LIN p,a,a ) by A19, AFF_1:6, AFF_1:7;
then ( a = a9 or b in A ) by A2, A8, A9, A50, A53, AFF_1:8, AFF_1:25;
then A54: LIN p,a,b9 by A5, A10, A14, A20, AFF_1:6, AFF_1:45;
( LIN p,a,b & LIN p,a,a ) by A19, AFF_1:6, AFF_1:7;
then a in P by A3, A10, A11, A43, A50, A54, AFF_1:8, AFF_1:25;
hence contradiction by A5, A8, A14, AFF_1:45; ::_thesis: verum
end;
A55: Line (a,c) is being_line by A25, AFF_1:24;
A56: ( Line (p,q) is being_line & q in Line (p,q) ) by A18, AFF_1:24;
A57: now__::_thesis:_not_Line_(a,c)_=_Line_(p,q)
assume Line (a,c) = Line (p,q) ; ::_thesis: contradiction
then A58: ( LIN q,c,a & LIN q,c,c ) by A56, A26, A31, AFF_1:21;
LIN q,c,b by A21, AFF_1:6;
hence contradiction by A16, A33, A58, AFF_1:8; ::_thesis: verum
end;
A59: c9 in Line (a9,c9) by A48, AFF_1:24;
A60: a9 in Line (a9,c9) by A48, AFF_1:24;
then consider x being Element of AP such that
A61: x in Line (a,c) and
A62: x in Line (a9,c9) by A32, A55, A49, A26, A31, A59, AFF_1:39, AFF_1:58;
A63: now__::_thesis:_not_x_=_c
assume x = c ; ::_thesis: contradiction
then Line (a9,c9) = C by A4, A12, A13, A37, A49, A59, A62, AFF_1:18;
hence contradiction by A6, A9, A15, A60, AFF_1:45; ::_thesis: verum
end;
A64: p in Line (p,q) by A18, AFF_1:24;
then A65: Line (a,c) // Line (p,q) by A18, A23, A25, A55, A56, A26, A31, AFF_1:38;
A66: now__::_thesis:_not_x_=_c9
assume x = c9 ; ::_thesis: contradiction
then Line (a,c) = C by A4, A12, A13, A37, A55, A31, A61, AFF_1:18;
hence contradiction by A6, A8, A15, A26, AFF_1:45; ::_thesis: verum
end;
Line (a,c) <> Line (a9,c9) by A32, A55, A26, A31, A60, A59, AFF_1:51;
then x in Line (p,q) by A1, A18, A25, A55, A49, A64, A56, A26, A31, A60, A59, A61, A62, A29, A27, A30, A28, A43, A63, A66, A46, A52, Def4;
hence contradiction by A65, A61, A57, AFF_1:45; ::_thesis: verum
end;