let AS be AffinSpace; :: thesis: for X, Y, X9 being Subset of AS
for P, Q being LINE of (IncProjSp_of AS) st Y is being_plane & X is being_line & X9 is being_line & X c= Y & X9 c= Y & P = [X,1] & Q = [X9,1] holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
let X, Y, X9 be Subset of AS; :: thesis: for P, Q being LINE of (IncProjSp_of AS) st Y is being_plane & X is being_line & X9 is being_line & X c= Y & X9 c= Y & P = [X,1] & Q = [X9,1] holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
let P, Q be LINE of (IncProjSp_of AS); :: thesis: ( Y is being_plane & X is being_line & X9 is being_line & X c= Y & X9 c= Y & P = [X,1] & Q = [X9,1] implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )
assume that
A1: Y is being_plane and
A2: X is being_line and
A3: X9 is being_line and
A4: X c= Y and
A5: X9 c= Y and
A6: P = [X,1] and
A7: Q = [X9,1] ; :: thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
A8: now :: thesis: ( X // X9 implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )
reconsider q = LDir X as POINT of (IncProjSp_of AS) by A2, Th20;
assume A9: X // X9 ; :: thesis: ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
take q = q; :: thesis: ( q on P & q on Q )
LDir X = LDir X9 by A2, A3, A9, Th11;
hence ( q on P & q on Q ) by A2, A3, A6, A7, Th30; :: thesis: verum
end;
now :: thesis: ( ex y being Element of AS st
( y in X & y in X9 ) implies ex q being Element of the Points of (IncProjSp_of AS) st
( q on P & q on Q ) )
given y being Element of AS such that A10: y in X and
A11: y in X9 ; :: 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 (IncProjSp_of AS) st
( q on P & q on Q ) by A1, A2, A3, A4, A5, A8, AFF_4:22; :: thesis: verum