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

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