let AS be AffinSpace; :: thesis: for M, X being Subset of st M is being_line & X is being_plane holds
ex q being Element of st
( q in X & not q in M )
let M, X be Subset of ; :: thesis: ( M is being_line & X is being_plane implies ex q being Element of st
( q in X & not q in M ) )
assume that
A1: M is being_line and
A2: X is being_plane ; :: thesis: ex q being Element of st
( q in X & not q in M )
consider a, b, c being Element of such that
A3: ( a in X & b in X ) and
A4: c in X and
A5: not LIN a,b,c by A2, Th34;
assume A6: for q being Element of holds
( not q in X or q in M ) ; :: thesis: contradiction
then A7: c in M by A4;
( a in M & b in M ) by A6, A3;
hence contradiction by A1, A5, A7, AFF_1:33; :: thesis: verum