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 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 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 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 Element of AS
; ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
A15:
b <> d
by A2, A4, A5, A6, A9, A12, A13, Lm2;
reconsider x = p as Element of AS by A14;
consider XM being Subset of AS such that
A16:
( ( M = [XM,1] & XM is being_line ) or ( M = [(PDir XM),2] & XM is being_plane ) )
by Th23;
consider XQ being Subset of AS such that
A17:
( ( Q = [XQ,1] & XQ is being_line ) or ( Q = [(PDir XQ),2] & XQ is being_plane ) )
by Th23;
consider XP being Subset of AS such that
A18:
( ( P = [XP,1] & XP is being_line ) or ( P = [(PDir XP),2] & XP is being_plane ) )
by Th23;
consider XN being Subset of AS such that
A19:
( ( N = [XN,1] & XN is being_line ) or ( N = [(PDir XN),2] & XN is being_plane ) )
by Th23;
A20:
x in XM
by A5, A16, Th26, Th27;
x in XN
by A6, A19, Th26, Th27;
then consider Y being Subset of AS such that
A21:
XM c= Y
and
A22:
XN c= Y
and
A23:
Y is being_plane
by A5, A6, A16, A19, A20, Th27, AFF_4:38;
A24:
a <> c
by A1, A3, A5, A6, A7, A11, A13, Lm2;
A25:
now ( P = [(PDir XP),2] & XP is being_plane implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )assume that A26:
P = [(PDir XP),2]
and A27:
XP is
being_plane
;
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )A28:
Y '||' XP
by A1, A3, A5, A6, A7, A8, A24, A16, A19, A20, A21, A22, A23, A26, A27, Lm8, Th27;
A29:
now ( Q = [XQ,1] & XQ is being_line implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )assume that A30:
Q = [XQ,1]
and A31:
XQ is
being_line
;
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )reconsider q =
LDir XQ as
POINT of
(IncProjSp_of AS) by A31, Th20;
take q =
q;
( q on P & q on Q )
XQ c= Y
by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A30, A31, Lm7, Th27;
then
XQ '||' Y
by A23, A31, AFF_4:42;
then
XQ '||' XP
by A23, A28, AFF_4:59, AFF_4:60;
hence
q on P
by A26, A27, A31, Th29;
q on Qthus
q on Q
by A30, A31, Th30;
verum end; now ( Q = [(PDir XQ),2] & XQ is being_plane implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )consider q,
r,
p9 being
POINT of
(IncProjSp_of AS) such that A32:
q on P
and
r on P
and
p9 on P
and
q <> r
and
r <> p9
and
p9 <> q
by Lm3;
assume that A33:
Q = [(PDir XQ),2]
and A34:
XQ is
being_plane
;
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )take q =
q;
( q on P & q on Q )thus
q on P
by A32;
q on Q
Y '||' XQ
by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A33, A34, Lm8, Th27;
then
XP '||' XQ
by A23, A27, A28, A34, AFF_4:61;
hence
q on Q
by A26, A27, A33, A34, A32, Th13;
verum end; hence
ex
q being
POINT of
(IncProjSp_of AS) st
(
q on P &
q on Q )
by A17, A29;
verum end;
now ( P = [XP,1] & XP is being_line implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )assume that A35:
P = [XP,1]
and A36:
XP is
being_line
;
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )A37:
XP c= Y
by A1, A3, A5, A6, A7, A8, A24, A16, A19, A20, A21, A22, A23, A35, A36, Lm7, Th27;
A38:
now ( Q = [(PDir XQ),2] & XQ is being_plane implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )A39:
XP '||' Y
by A23, A36, A37, AFF_4:42;
reconsider q =
LDir XP as
POINT of
(IncProjSp_of AS) by A36, Th20;
assume that A40:
Q = [(PDir XQ),2]
and A41:
XQ is
being_plane
;
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )take q =
q;
( q on P & q on Q )thus
q on P
by A35, A36, Th30;
q on Q
Y '||' XQ
by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A40, A41, Lm8, Th27;
then
XP '||' XQ
by A23, A39, AFF_4:59, AFF_4:60;
hence
q on Q
by A36, A40, A41, Th29;
verum end; now ( Q = [XQ,1] & XQ is being_line implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )assume that A42:
Q = [XQ,1]
and A43:
XQ is
being_line
;
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
XQ c= Y
by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A42, A43, Lm7, Th27;
hence
ex
q being
POINT of
(IncProjSp_of AS) st
(
q on P &
q on Q )
by A23, A35, A36, A37, A42, A43, Th43;
verum end; hence
ex
q being
POINT of
(IncProjSp_of AS) st
(
q on P &
q on Q )
by A17, A38;
verum end;
hence
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
by A18, A25; verum