let AS be AffinSpace; :: thesis: for M, N, X 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 M, N, X 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 and

A3: N is being_line and

A4: ( 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

A5: K is being_line and

A6: P is being_line and

not K // P and

A7: X = Plane (K,P) by A1;

( q in M & q in N ) ) by A8, AFF_1:44; :: thesis: verum

ex q being Element of AS st

( q in M & q in N )

let M, N, X 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 and

A3: N is being_line and

A4: ( 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

A5: K is being_line and

A6: P is being_line and

not K // P and

A7: X = Plane (K,P) by A1;

A8: now :: thesis: ( not K // N & not M // N implies ex q being Element of AS st

( q in M & q in N ) )

( q in M & q in N ) )

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 A3, A4, A5, A6, A7, Th20;

then ( N // M or ex q being Element of AS st

( q in N & q in M ) ) by A2, A3, A5, Th21;

hence ( M // N or ex q being Element of AS st

( q in M & q in N ) ) ; :: thesis: verum

end;( q in M & q in N ) )

then M c= Plane (K,N) by A3, A4, A5, A6, A7, Th20;

then ( N // M or ex q being Element of AS st

( q in N & q in M ) ) by A2, A3, A5, Th21;

hence ( M // N or ex q being Element of AS st

( q in M & q in N ) ) ; :: thesis: verum

now :: thesis: ( not K // M & not M // N implies ex q being Element of AS st

( q in M & q in N ) )

hence
( M // N or ex q being Element of AS st ( q in M & q in N ) )

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, A4, A5, A6, A7, Th20;

hence ( M // N or ex q being Element of AS st

( q in M & q in N ) ) by A2, A3, A5, Th21; :: thesis: verum

end;( q in M & q in N ) )

then N c= Plane (K,M) by A2, A4, A5, A6, A7, Th20;

hence ( M // N or ex q being Element of AS st

( q in M & q in N ) ) by A2, A3, A5, Th21; :: thesis: verum

( q in M & q in N ) ) by A8, AFF_1:44; :: thesis: verum