let AS be AffinSpace; :: thesis: for M, X being Subset of AS st M is being_line & X is being_plane holds
ex q being Element of AS st
( q in X & not q in M )
let M, X be Subset of AS; :: thesis: ( M is being_line & X is being_plane implies ex q being Element of AS 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 AS st
( q in X & not q in M )
consider a, b, c being Element of AS 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 AS 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:21; :: thesis: verum