let AS be AffinSpace; :: thesis: for Y, X, X' being Subset of
for P, Q being LINE of st Y is being_plane & X is being_line & X' is being_line & X c= Y & X' c= Y & P = [X,1] & Q = [X',1] holds
ex q being POINT of st
( q on P & q on Q )
let Y, X, X' be Subset of ; :: thesis: for P, Q being LINE of st Y is being_plane & X is being_line & X' is being_line & X c= Y & X' c= Y & P = [X,1] & Q = [X',1] holds
ex q being POINT of st
( q on P & q on Q )
let P, Q be LINE of ; :: thesis: ( Y is being_plane & X is being_line & X' is being_line & X c= Y & X' c= Y & P = [X,1] & Q = [X',1] implies ex q being POINT of st
( q on P & q on Q ) )
assume that
A1: Y is being_plane and
A2: X is being_line and
A3: X' is being_line and
A4: X c= Y and
A5: X' c= Y and
A6: P = [X,1] and
A7: Q = [X',1] ; :: thesis: ex q being POINT of st
( q on P & q on Q )

A8: now

reconsider q = LDir X as POINT of by A2, Th20;
assume A9: X // X' ; :: thesis: ex q being POINT of st
( q on P & q on Q )
take q = q; :: thesis: ( q on P & q on Q )
LDir X = LDir X' by A2, A3, A9, Th11;
hence ( q on P & q on Q ) by A2, A3, A6, A7, Th30; :: thesis: verum

end;

now

given y being Element of such that A10: y in X and
A11: y in X' ; :: thesis: ex q being Element of the Points of (IncProjSp_of AS) st
( q on P & q on Q )
reconsider q = y as Element of the Points of (IncProjSp_of AS) by Th20;
take q = q; :: thesis: ( q on P & q on Q )
thus ( q on P & q on Q ) by A2, A3, A6, A7, A10, A11, Th26; :: thesis: verum

end;

hence ex q being POINT of st
( q on P & q on Q ) by A1, A2, A3, A4, A5, A8, AFF_4:22; :: thesis: verum