let AS be AffinSpace; :: thesis: for a being Element of AS
for X being Subset of AS st X is being_plane holds
ex b, c being Element of AS st
( b in X & c in X & not LIN a,b,c )
let a be Element of AS; :: thesis: for X being Subset of AS st X is being_plane holds
ex b, c being Element of AS st
( b in X & c in X & not LIN a,b,c )
let X be Subset of AS; :: thesis: ( X is being_plane implies ex b, c being Element of AS st
( b in X & c in X & not LIN a,b,c ) )
assume X is being_plane ; :: thesis: ex b, c being Element of AS st
( b in X & c in X & not LIN a,b,c )
then consider p, q, r being Element of AS such that
A1: ( p in X & q in X ) and
A2: r in X and
A3: not LIN p,q,r by Th34;
now :: thesis: ( LIN a,r,p & LIN a,r,q implies ex b, c being Element of AS st
( b in X & c in X & not LIN a,b,c ) )
assume A4: ( LIN a,r,p & LIN a,r,q ) ; :: thesis: ex b, c being Element of AS st
( b in X & c in X & not LIN a,b,c )
take b = p; :: thesis: ex c being Element of AS st
( b in X & c in X & not LIN a,b,c )
take c = q; :: thesis: ( b in X & c in X & not LIN a,b,c )
thus ( b in X & c in X ) by A1; :: thesis: not LIN a,b,c
LIN a,r,r by AFF_1:7;
then a = r by A3, A4, AFF_1:8;
hence not LIN a,b,c by A3, AFF_1:6; :: thesis: verum
end;
hence ex b, c being Element of AS st
( b in X & c in X & not LIN a,b,c ) by A1, A2; :: thesis: verum