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;

( b in X & c in X & not LIN a,b,c ) by A1, A2; :: thesis: verum

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 ) )

hence
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;( 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

( b in X & c in X & not LIN a,b,c ) by A1, A2; :: thesis: verum