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 M9 = [M,2], N9 = [N,2], P9 = [P,2], Q9 = [Q,2] as LINE of (IncProjSp_of AS) by Th25;
reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p as POINT of (IncProjSp_of AS) by Th22;
A14:
b9 on M9
by A2, Th37;
A15:
M9 <> N9
proof
assume
M9 = N9
;
contradiction
then M =
[N,2] `1
.=
N
;
hence
contradiction
by A13;
verum
end;
A16:
d9 on N9
by A4, Th37;
A17:
c9 on N9
by A3, Th37;
A18:
c9 on P9
by A8, Th37;
A19:
a9 on P9
by A7, Th37;
A20:
p9 on N9
by A6, Th37;
A21:
p9 on M9
by A5, Th37;
A22:
not p9 on Q9
by A12, Th37;
A23:
not p9 on P9
by A11, Th37;
A24:
d9 on Q9
by A10, Th37;
A25:
b9 on Q9
by A9, Th37;
a9 on M9
by A1, Th37;
then consider q9 being POINT of (IncProjSp_of AS) such that
A26:
q9 on P9
and
A27:
q9 on Q9
by A14, A17, A16, A21, A20, A19, A18, A25, A24, A23, A22, A15, Lm12;
[q9,[P,2]] in the Inc of (IncProjSp_of AS)
by A26, INCSP_1:def 1;
then reconsider q = q9 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