let AS be AffinSpace; :: thesis:
let a, b, c, d, p be POINT of (IncProjSp_of AS); :: thesis:
let M, N, P, Q be LINE of (IncProjSp_of AS); :: thesis:
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 ; :: thesis:
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 :: thesis:

assume that
A26: P = [(PDir XP),2] and
A27: XP is being_plane ; :: thesis:
A28: Y '||' XP by A1, A3, A5, A6, A7, A8, A24, A16, A19, A20, A21, A22, A23, A26, A27, Lm8, Th27;

A29: now :: thesis:

assume that
A30: Q = [XQ,1] and
A31: XQ is being_line ; :: thesis:
reconsider q = LDir XQ as POINT of (IncProjSp_of AS) by A31, Th20;
take q = q; :: thesis:
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; :: thesis:
thus q on Q by A30, A31, Th30; :: thesis:

end;

now :: thesis:

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 ; :: thesis:
take q = q; :: thesis:
thus q on P by A32; :: thesis:
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; :: thesis:

end;

hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A17, A29; :: thesis:

end;

now :: thesis:

assume that
A35: P = [XP,1] and
A36: XP is being_line ; :: thesis:
A37: XP c= Y by A1, A3, A5, A6, A7, A8, A24, A16, A19, A20, A21, A22, A23, A35, A36, Lm7, Th27;

A38: now :: thesis:

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 ; :: thesis:
take q = q; :: thesis:
thus q on P by A35, A36, Th30; :: thesis:
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; :: thesis:

end;

now :: thesis:

assume that
A42: Q = [XQ,1] and
A43: XQ is being_line ; :: thesis:
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; :: thesis:

end;

hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A17, A38; :: thesis:

end;

hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A18, A25; :: thesis: