let AS be AffinSpace; for a, b, c, d, p being POINT of (IncProjSp_of AS)
for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is not Element of AS & ( a is Element of AS or b is Element of AS or c is Element of AS or d is Element of AS ) holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
let a, b, c, d, p be POINT of (IncProjSp_of AS); for M, N, P, Q being LINE of (IncProjSp_of AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is not Element of AS & ( a is Element of AS or b is Element of AS or c is Element of AS or d is Element of AS ) holds
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
let M, N, P, Q be LINE of (IncProjSp_of AS); ( a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is not Element of AS & ( a is Element of AS or b is Element of AS or c is Element of AS or d is Element of AS ) implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )
assume that
A1:
a on M
and
A2:
b on M
and
A3:
c on N
and
A4:
d on N
and
A5:
p on M
and
A6:
p on N
and
A7:
a on P
and
A8:
c on P
and
A9:
b on Q
and
A10:
d on Q
and
A11:
not p on P
and
A12:
not p on Q
and
A13:
M <> N
and
A14:
p is not Element of AS
and
A15:
( a is Element of AS or b is Element of AS or c is Element of AS or d is Element of AS )
; ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
now ( ( b is Element of AS or d is Element of AS ) implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )assume
(
b is
Element of
AS or
d is
Element of
AS )
;
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )then
ex
q being
POINT of
(IncProjSp_of AS) st
(
q on Q &
q on P )
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, Lm10;
hence
ex
q being
POINT of
(IncProjSp_of AS) st
(
q on P &
q on Q )
;
verum end;
hence
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, Lm10; verum