let AS be AffinSpace; :: thesis: for X, M, N being Subset of AS st X is being_plane & M is being_line & N is being_line & M c= X & N c= X & not M // N holds
ex q being Element of AS st
( q in M & q in N )
let X, M, N be Subset of AS; :: thesis: ( X is being_plane & M is being_line & N is being_line & M c= X & N c= X & not M // N implies ex q being Element of AS st
( q in M & q in N ) )
assume that
A1: X is being_plane and
A2: ( M is being_line & N is being_line ) and
A3: ( M c= X & N c= X ) ; :: thesis: ( M // N or ex q being Element of AS st
( q in M & q in N ) )
consider K, P being Subset of AS such that
A4: ( K is being_line & P is being_line ) and
A5: not K // P and
A6: X = Plane K,P by A1, Def2;

A7: now

assume not K // M ; :: thesis: ( M // N or ex q being Element of AS st
( q in M & q in N ) )
then N c= Plane K,M by A2, A3, A4, A5, A6, Th20;
hence ( M // N or ex q being Element of AS st
( q in M & q in N ) ) by A2, A4, Th21; :: thesis: verum

end;

now

assume not K // N ; :: thesis: ( M // N or ex q being Element of AS st
( q in M & q in N ) )
then M c= Plane K,N by A2, A3, A4, A5, A6, Th20;
then ( N // M or ex q being Element of AS st
( q in N & q in M ) ) by A2, A4, Th21;
hence ( M // N or ex q being Element of AS st
( q in M & q in N ) ) ; :: thesis: verum

end;

hence ( M // N or ex q being Element of AS st
( q in M & q in N ) ) by A7, AFF_1:58; :: thesis: verum