let AS be AffinSpace; for a, b, c, d, p being Element of the Points of (ProjHorizon AS)
for M, N, P, Q being Element of the Lines of (ProjHorizon 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 holds
ex q being Element of the Points of (ProjHorizon AS) st
( q on P & q on Q )
let a, b, c, d, p be Element of the Points of (ProjHorizon AS); for M, N, P, Q being Element of the Lines of (ProjHorizon 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 holds
ex q being Element of the Points of (ProjHorizon AS) st
( q on P & q on Q )
let M, N, P, Q be Element of the Lines of (ProjHorizon 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 implies ex q being Element of the Points of (ProjHorizon 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
; ex q being Element of the Points of (ProjHorizon AS) st
( q on P & q on Q )
reconsider M' = [M,2], N' = [N,2], P' = [P,2], Q' = [Q,2] as LINE of by Th25;
reconsider a' = a, b' = b, c' = c, d' = d, p' = p as POINT of by Th22;
A14:
b' on M'
by A2, Th37;
A15:
M' <> N'
A16:
d' on N'
by A4, Th37;
A17:
c' on N'
by A3, Th37;
A18:
c' on P'
by A8, Th37;
A19:
a' on P'
by A7, Th37;
A20:
p' on N'
by A6, Th37;
A21:
p' on M'
by A5, Th37;
A22:
not p' on Q'
by A12, Th37;
A23:
not p' on P'
by A11, Th37;
A24:
d' on Q'
by A10, Th37;
A25:
b' on Q'
by A9, Th37;
a' on M'
by A1, Th37;
then consider q' being POINT of such that
A26:
q' on P'
and
A27:
q' on Q'
by A14, A17, A16, A21, A20, A19, A18, A25, A24, A23, A22, A15, Lm12;
[q',[P,2]] in the Inc of (IncProjSp_of AS)
by A26, INCSP_1:def 1;
then reconsider q = q' as Element of the Points of (ProjHorizon AS) by Th42;
take
q
; ( q on P & q on Q )
thus
( q on P & q on Q )
by A26, A27, Th37; verum