let AS be AffinSpace; :: thesis: for X being Subset of AS st X is being_plane holds
ex a, b, c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c )
let X be Subset of AS; :: thesis: ( X is being_plane implies ex a, b, c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c ) )
assume X is being_plane ; :: thesis: ex a, b, c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c )
then consider K, P being Subset of AS such that
A1: K is being_line and
A2: P is being_line and
A3: not K // P and
A4: X = Plane (K,P) ;
consider a, b being Element of AS such that
A5: a in P and
A6: b in P and
A7: a <> b by A2, AFF_1:19;
set Q = a * K;
consider c being Element of AS such that
A8: a <> c and
A9: c in a * K by A1, Th27, AFF_1:20;
take a ; :: thesis: ex b, c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c )
take b ; :: thesis: ex c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c )
take c ; :: thesis: ( a in X & b in X & c in X & not LIN a,b,c )
A10: P c= Plane (K,P) by A1, Th14;
hence ( a in X & b in X ) by A4, A5, A6; :: thesis: ( c in X & not LIN a,b,c )
A11: ( K // a * K & a in a * K ) by A1, Def3;
then a * K c= Plane (K,P) by A5, A10, Lm4;
hence c in X by A4, A9; :: thesis: not LIN a,b,c
A12: a * K is being_line by A1, Th27;
thus not LIN a,b,c :: thesis: verum

proof

assume LIN a,b,c ; :: thesis: contradiction
then c in P by A2, A5, A6, A7, AFF_1:25;
hence contradiction by A2, A3, A5, A11, A12, A8, A9, AFF_1:18; :: thesis: verum

end;