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

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