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;
A8: now :: thesis: ( not K // N & not M // N implies ex q being Element of AS st
( 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;
now :: thesis: ( not K // M & not M // N implies 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;
hence ( M // N or ex q being Element of AS st
( q in M & q in N ) ) by A8, AFF_1:44; :: thesis: verum