let AS be AffinSpace; :: thesis: for a, b, c, a', b' being Element of
for X being Subset of st not LIN a,b,c & a,b // a',b' & a in X & b in X & c in X & X is being_plane & a' in X holds
ex c' being Element of st
( a,c // a',c' & b,c // b',c' )
let a, b, c, a', b' be Element of ; :: thesis: for X being Subset of st not LIN a,b,c & a,b // a',b' & a in X & b in X & c in X & X is being_plane & a' in X holds
ex c' being Element of st
( a,c // a',c' & b,c // b',c' )
let X be Subset of ; :: thesis: ( not LIN a,b,c & a,b // a',b' & a in X & b in X & c in X & X is being_plane & a' in X implies ex c' being Element of st
( a,c // a',c' & b,c // b',c' ) )
assume that
A1: not LIN a,b,c and
A2: a,b // a',b' and
A3: a in X and
A4: b in X and
A5: c in X and
A6: X is being_plane and
A7: a' in X ; :: thesis: ex c' being Element of st
( a,c // a',c' & b,c // b',c' )
set C = Line b,c;
set P = Line a,c;
set P' = a' * (Line a,c);
set C' = b' * (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 // b' * (Line b,c) by Def3;
a <> b by A1, AFF_1:16;
then b' in X by A2, A3, A4, A6, A7, Th29;
then A11: b' * (Line b,c) c= X by A4, A5, A6, A8, A9, Th19, Th28;
A12: c in Line a,c by AFF_1:26;
A13: b' * (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: a' * (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 // a' * (Line a,c) by A16, Def3;
A20: not b' * (Line b,c) // a' * (Line a,c)

proof

assume b' * (Line b,c) // a' * (Line a,c) ; :: thesis: contradiction
then b' * (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;

a' * (Line a,c) c= X by A3, A5, A6, A7, A15, A16, Th19, Th28;
then consider c' being Element of such that
A21: c' in b' * (Line b,c) and
A22: c' in a' * (Line a,c) by A6, A17, A13, A20, A11, Th22;
b' in b' * (Line b,c) by A9, Def3;
then A23: b,c // b',c' by A18, A10, A21, AFF_1:53;
a' in a' * (Line a,c) by A16, Def3;
then a,c // a',c' by A14, A12, A19, A22, AFF_1:53;
hence ex c' being Element of st
( a,c // a',c' & b,c // b',c' ) by A23; :: thesis: verum