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))

proof

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;

a9 * (Line (a,c)) c= X by A3, A5, A6, A7, A15, A16, Th19, Th28;
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