let AS be AffinSpace; :: thesis: for a, b, c, a9, b9 being Element of AS st not LIN a,b,c & a9 <> b9 & a,b // a9,b9 holds
ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
let a, b, c, a9, b9 be Element of AS; :: thesis: ( not LIN a,b,c & a9 <> b9 & a,b // a9,b9 implies ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) )
assume that
A1: not LIN a,b,c and
A2: a9 <> b9 and
A3: a,b // a9,b9 ; :: thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
now :: thesis: ( AS is not AffinPlane implies ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) )
consider X being Subset of AS such that
A4: a in X and
A5: b in X and
A6: c in X and
A7: X is being_plane by Th37;
assume A8: AS is not AffinPlane ; :: thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
now :: thesis: ( not a9 in X implies ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) )
set A = Line (a,a9);
set P = Line (b,b9);
set AB = Line (a,b);
set AB9 = Line (a9,b9);
A9: a in Line (a,b) by AFF_1:15;
assume A10: not a9 in X ; :: thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
then A11: Line (a,a9) is being_line by A4, AFF_1:def 3;
A12: a <> b by A1, AFF_1:7;
then A13: Line (a,b) c= X by A4, A5, A7, Th19;
A14: Line (a,b) // Line (a9,b9) by A2, A3, A12, AFF_1:37;
then consider Y being Subset of AS such that
A15: Line (a,b) c= Y and
A16: Line (a9,b9) c= Y and
A17: Y is being_plane by Th39;
A18: b in Line (a,b) by AFF_1:15;
A19: a9 in Line (a9,b9) by AFF_1:15;
then A20: Line (a,a9) c= Y by A4, A10, A9, A15, A16, A17, Th19;
A21: b9 in Line (a9,b9) by AFF_1:15;
A22: not b9 in X
proof
assume b9 in X ; :: thesis: contradiction
then Line (a9,b9) c= X by A7, A21, A14, A13, Th23;
hence contradiction by A10, A19; :: thesis: verum
end;
then A23: Line (b,b9) is being_line by A5, AFF_1:def 3;
A24: b9 in Line (b,b9) by AFF_1:15;
A25: a in Line (a,a9) by AFF_1:15;
A26: a <> c by A1, AFF_1:7;
A27: b in Line (b,b9) by AFF_1:15;
A28: a9 in Line (a,a9) by AFF_1:15;
A29: Line (a,b) is being_line by A12, AFF_1:def 3;
A30: Line (a,a9) <> Line (b,b9)
proof
assume Line (a,a9) = Line (b,b9) ; :: thesis: contradiction
then Line (a,a9) = Line (a,b) by A12, A9, A18, A29, A11, A25, A27, AFF_1:18;
hence contradiction by A10, A13, A28; :: thesis: verum
end;
A31: now :: thesis: ( Line (a,a9) // Line (b,b9) implies ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) )
set C = c * (Line (a,a9));
assume A32: Line (a,a9) // Line (b,b9) ; :: thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
A33: c in c * (Line (a,a9)) by A11, Def3;
A34: Line (a,a9) <> c * (Line (a,a9))
proof
assume Line (a,a9) = c * (Line (a,a9)) ; :: thesis: contradiction
then Line (a,a9) = Line (a,c) by A26, A11, A25, A33, AFF_1:57;
then Line (a,a9) c= X by A4, A6, A7, A26, Th19;
hence contradiction by A10, A28; :: thesis: verum
end;
A35: Line (a,a9) // c * (Line (a,a9)) by A11, Def3;
then consider c9 being Element of AS such that
A36: c9 in c * (Line (a,a9)) and
A37: a,c // a9,c9 by A25, A28, A33, Lm2;
c * (Line (a,a9)) is being_line by A11, Th27;
then b,c // b9,c9 by A3, A8, A11, A23, A25, A28, A27, A24, A30, A32, A33, A35, A36, A37, A34, Th51;
hence ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A37; :: thesis: verum
end;
A38: a9 in Y by A19, A16;
A39: now :: thesis: ( ex q being Element of AS st
( q in Line (a,a9) & q in Line (b,b9) ) implies ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) )
given q being Element of AS such that A40: q in Line (a,a9) and
A41: q in Line (b,b9) ; :: thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
A42: q <> a
proof
assume q = a ; :: thesis: contradiction
then Line (a,b) = Line (b,b9) by A12, A9, A18, A29, A23, A27, A41, AFF_1:18;
hence contradiction by A13, A22, A24; :: thesis: verum
end;
A43: q <> b
proof
assume q = b ; :: thesis: contradiction
then Line (a,b) = Line (a,a9) by A12, A9, A18, A29, A11, A25, A40, AFF_1:18;
hence contradiction by A10, A13, A28; :: thesis: verum
end;
set C = Line (q,c);
A44: c in Line (q,c) by AFF_1:15;
A45: Line (a,a9) <> Line (q,c)
proof
assume Line (a,a9) = Line (q,c) ; :: thesis: contradiction
then Line (a,a9) = Line (a,c) by A26, A11, A25, A44, AFF_1:57;
then Line (a,a9) c= X by A4, A6, A7, A26, Th19;
hence contradiction by A10, A28; :: thesis: verum
end;
LIN q,a,a9 by A11, A25, A28, A40, AFF_1:21;
then consider c9 being Element of AS such that
A46: LIN q,c,c9 and
A47: a,c // a9,c9 by A42, Th1;
A48: q <> c by A1, A4, A5, A6, A7, A10, A9, A18, A15, A17, A38, A20, A40, Th25;
then A49: ( q in Line (q,c) & Line (q,c) is being_line ) by AFF_1:15, AFF_1:def 3;
then c9 in Line (q,c) by A48, A44, A46, AFF_1:25;
then b,c // b9,c9 by A3, A8, A11, A23, A25, A28, A27, A24, A30, A40, A41, A42, A43, A48, A44, A49, A47, A45, Th49;
hence ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A47; :: thesis: verum
end;
Line (b,b9) c= Y by A5, A18, A21, A22, A15, A16, A17, Th19;
hence ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A17, A11, A23, A20, A31, A39, Th22; :: thesis: verum
end;
hence ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A1, A3, A4, A5, A6, A7, Lm12; :: thesis: verum
end;
hence ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A1, Th53; :: thesis: verum