let AS be AffinSpace; :: thesis: for a, b, c, a9, b9 being Element of AS

for X being Subset of AS st not LIN a,b,c & a,b // a9,b9 & a in X & b in X & c in X & X is being_plane & a9 in X 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: for X being Subset of AS st not LIN a,b,c & a,b // a9,b9 & a in X & b in X & c in X & X is being_plane & a9 in X holds

ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 )

let X be Subset of AS; :: thesis: ( not LIN a,b,c & a,b // a9,b9 & a in X & b in X & c in X & X is being_plane & a9 in X 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: a,b // a9,b9 and

A3: a in X and

A4: b in X and

A5: c in X and

A6: X is being_plane and

A7: a9 in X ; :: thesis: ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 )

set C = Line (b,c);

set P = Line (a,c);

set P9 = a9 * (Line (a,c));

set C9 = b9 * (Line (b,c));

A8: b <> c by A1, AFF_1:7;

then A9: Line (b,c) is being_line by AFF_1:def 3;

then A10: Line (b,c) // b9 * (Line (b,c)) by Def3;

a <> b by A1, AFF_1:7;

then b9 in X by A2, A3, A4, A6, A7, Th29;

then A11: b9 * (Line (b,c)) c= X by A4, A5, A6, A8, A9, Th19, Th28;

A12: c in Line (a,c) by AFF_1:15;

A13: b9 * (Line (b,c)) is being_line by A9, Th27;

A14: a in Line (a,c) by AFF_1:15;

A15: c <> a by A1, AFF_1:7;

then A16: Line (a,c) is being_line by AFF_1:def 3;

then A17: a9 * (Line (a,c)) is being_line by Th27;

A18: ( b in Line (b,c) & c in Line (b,c) ) by AFF_1:15;

A19: Line (a,c) // a9 * (Line (a,c)) by A16, Def3;

A20: not b9 * (Line (b,c)) // a9 * (Line (a,c))

then consider c9 being Element of AS such that

A21: c9 in b9 * (Line (b,c)) and

A22: c9 in a9 * (Line (a,c)) by A6, A17, A13, A20, A11, Th22;

b9 in b9 * (Line (b,c)) by A9, Def3;

then A23: b,c // b9,c9 by A18, A10, A21, AFF_1:39;

a9 in a9 * (Line (a,c)) by A16, Def3;

then a,c // a9,c9 by A14, A12, A19, A22, AFF_1:39;

hence ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 ) by A23; :: thesis: verum

for X being Subset of AS st not LIN a,b,c & a,b // a9,b9 & a in X & b in X & c in X & X is being_plane & a9 in X 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: for X being Subset of AS st not LIN a,b,c & a,b // a9,b9 & a in X & b in X & c in X & X is being_plane & a9 in X holds

ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 )

let X be Subset of AS; :: thesis: ( not LIN a,b,c & a,b // a9,b9 & a in X & b in X & c in X & X is being_plane & a9 in X 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: a,b // a9,b9 and

A3: a in X and

A4: b in X and

A5: c in X and

A6: X is being_plane and

A7: a9 in X ; :: thesis: ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 )

set C = Line (b,c);

set P = Line (a,c);

set P9 = a9 * (Line (a,c));

set C9 = b9 * (Line (b,c));

A8: b <> c by A1, AFF_1:7;

then A9: Line (b,c) is being_line by AFF_1:def 3;

then A10: Line (b,c) // b9 * (Line (b,c)) by Def3;

a <> b by A1, AFF_1:7;

then b9 in X by A2, A3, A4, A6, A7, Th29;

then A11: b9 * (Line (b,c)) c= X by A4, A5, A6, A8, A9, Th19, Th28;

A12: c in Line (a,c) by AFF_1:15;

A13: b9 * (Line (b,c)) is being_line by A9, Th27;

A14: a in Line (a,c) by AFF_1:15;

A15: c <> a by A1, AFF_1:7;

then A16: Line (a,c) is being_line by AFF_1:def 3;

then A17: a9 * (Line (a,c)) is being_line by Th27;

A18: ( b in Line (b,c) & c in Line (b,c) ) by AFF_1:15;

A19: Line (a,c) // a9 * (Line (a,c)) by A16, Def3;

A20: not b9 * (Line (b,c)) // a9 * (Line (a,c))

proof

a9 * (Line (a,c)) c= X
by A3, A5, A6, A7, A15, A16, Th19, Th28;
assume
b9 * (Line (b,c)) // a9 * (Line (a,c))
; :: thesis: contradiction

then b9 * (Line (b,c)) // Line (a,c) by A19, AFF_1:44;

then Line (b,c) // Line (a,c) by A10, AFF_1:44;

then b in Line (a,c) by A12, A18, AFF_1:45;

hence contradiction by A1, A14, A12, A16, AFF_1:21; :: thesis: verum

end;then b9 * (Line (b,c)) // Line (a,c) by A19, AFF_1:44;

then Line (b,c) // Line (a,c) by A10, AFF_1:44;

then b in Line (a,c) by A12, A18, AFF_1:45;

hence contradiction by A1, A14, A12, A16, AFF_1:21; :: thesis: verum

then consider c9 being Element of AS such that

A21: c9 in b9 * (Line (b,c)) and

A22: c9 in a9 * (Line (a,c)) by A6, A17, A13, A20, A11, Th22;

b9 in b9 * (Line (b,c)) by A9, Def3;

then A23: b,c // b9,c9 by A18, A10, A21, AFF_1:39;

a9 in a9 * (Line (a,c)) by A16, Def3;

then a,c // a9,c9 by A14, A12, A19, A22, AFF_1:39;

hence ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 ) by A23; :: thesis: verum