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 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 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 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
; ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
reconsider x = a as Element of AS by A15;
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;
A17:
x in XM
by A1, A16, Th26, Th27;
A18:
b <> d
by A2, A4, A5, A6, A9, A12, A13, Lm2;
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;
consider XP being Subset of AS such that
A20:
( ( P = [XP,1] & XP is being_line ) or ( P = [(PDir XP),2] & XP is being_plane ) )
by Th23;
A21:
x = a
;
then reconsider y = b as Element of AS by A1, A2, A5, A9, A12, A14, A16, Th27, Th35;
A22:
y in XM
by A2, A16, Th26, Th27;
consider X being Subset of AS such that
A23:
p = LDir X
and
A24:
X is being_line
by A14, Th20;
consider XQ being Subset of AS such that
A25:
( ( Q = [XQ,1] & XQ is being_line ) or ( Q = [(PDir XQ),2] & XQ is being_plane ) )
by Th23;
A26:
x in XP
by A7, A20, Th26, Th27;
then consider Y being Subset of AS such that
A27:
XM c= Y
and
A28:
XP c= Y
and
A29:
Y is being_plane
by A1, A7, A16, A20, A17, Th27, AFF_4:38;
A30:
y = b
;
A31:
X '||' XM
by A1, A5, A23, A24, A16, A21, Th27, Th28;
then A32:
X // XM
by A1, A24, A16, A21, Th27, AFF_4:40;
A33:
y in XQ
by A9, A25, Th26, Th27;
A34:
not XM // XP
by A1, A5, A7, A11, A16, A20, A17, A26, Th27, AFF_1:45;
A35:
now ( N = [XN,1] & XN is being_line implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )A36:
X // XM
by A1, A24, A16, A21, A31, Th27, AFF_4:40;
assume that A37:
N = [XN,1]
and A38:
XN is
being_line
;
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
X '||' XN
by A6, A23, A24, A37, A38, Th28;
then
X // XN
by A24, A38, AFF_4:40;
then A39:
XM // XN
by A36, AFF_1:44;
c is
Element of
AS
proof
assume
c is not
Element of
AS
;
contradiction
then
c = LDir XN
by A3, A37, A38, Th34;
then
XN '||' XP
by A7, A8, A20, A21, A38, Th27, Th28;
then
XN // XP
by A7, A20, A21, A38, Th27, AFF_4:40;
hence
contradiction
by A34, A39, AFF_1:44;
verum
end; then reconsider z =
c as
Element of
AS ;
z in XN
by A3, A37, Th26;
then A40:
XN = z * XM
by A1, A16, A21, A39, Th27, AFF_4:def 3;
A41:
not
XN // XQ
proof
assume
XN // XQ
;
contradiction
then
XM // XQ
by A39, AFF_1:44;
hence
contradiction
by A2, A5, A9, A12, A16, A25, A33, A22, Th27, AFF_1:45;
verum
end; now d is Element of ASassume
d is not
Element of
AS
;
contradictionthen consider Xd being
Subset of
AS such that A42:
d = LDir Xd
and A43:
Xd is
being_line
by Th20;
Xd '||' XN
by A4, A37, A38, A42, A43, Th28;
then A44:
Xd // XN
by A38, A43, AFF_4:40;
Xd '||' XQ
by A9, A10, A25, A30, A42, A43, Th27, Th28;
then
Xd // XQ
by A9, A25, A30, A43, Th27, AFF_4:40;
hence
contradiction
by A41, A44, AFF_1:44;
verum end; then reconsider w =
d as
Element of
AS ;
w in XQ
by A10, A25, Th26, Th27;
then A45:
XQ = Line (
y,
w)
by A9, A18, A25, A33, Th27, AFF_1:57;
z in XP
by A8, A20, Th26, Th27;
then A46:
XN c= Y
by A1, A16, A21, A27, A28, A29, A40, Th27, AFF_4:28;
w in XN
by A4, A37, Th26;
then
XQ c= Y
by A18, A27, A29, A22, A46, A45, AFF_4:19;
hence
ex
q being
POINT of
(IncProjSp_of AS) st
(
q on P &
q on Q )
by A7, A9, A20, A25, A21, A28, A29, A30, Th27, Th43;
verum end;
A47:
XP '||' Y
by A7, A20, A21, A28, A29, Th27, AFF_4:42;
A48:
XM '||' Y
by A1, A16, A21, A27, A29, Th27, AFF_4:42;
now ( N = [(PDir XN),2] & XN is being_plane implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )assume that A49:
N = [(PDir XN),2]
and A50:
XN is
being_plane
;
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
c is not
Element of
AS
by A3, A49, Th27;
then
c = LDir XP
by A7, A8, A20, A21, Th27, Th34;
then A51:
XP '||' XN
by A3, A7, A20, A21, A49, A50, Th27, Th29;
d is not
Element of
AS
by A4, A49, Th27;
then
d = LDir XQ
by A9, A10, A25, A30, Th27, Th34;
then A52:
XQ '||' XN
by A4, A9, A25, A30, A49, A50, Th27, Th29;
X '||' XN
by A6, A23, A24, A49, A50, Th29;
then
XM '||' XN
by A32, AFF_4:56;
then
XN '||' Y
by A1, A5, A7, A11, A16, A20, A17, A26, A29, A48, A47, A50, A51, Th5, Th27, AFF_1:45;
then
XQ '||' Y
by A50, A52, AFF_4:59, AFF_4:60;
then
XQ c= Y
by A9, A25, A27, A29, A33, A22, Th27, AFF_4:43;
hence
ex
q being
POINT of
(IncProjSp_of AS) st
(
q on P &
q on Q )
by A7, A9, A20, A25, A21, A28, A29, A30, Th27, Th43;
verum end;
hence
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
by A19, A35; verum