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:16;
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:16;
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:26;
A13: b9 * (Line b,c) is being_line by A9, Th27;
A14: a in Line a,c by AFF_1:26;
A15: c <> a by A1, AFF_1:16;
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:26;
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:58;
then Line b,c // Line a,c by A10, AFF_1:58;
then b in Line a,c by A12, A18, AFF_1:59;
hence contradiction by A1, A14, A12, A16, AFF_1:33; :: 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:53;
a9 in a9 * (Line a,c) by A16, Def3;
then a,c // a9,c9 by A14, A12, A19, A22, AFF_1:53;
hence ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A23; :: thesis: verum