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 ; :: thesis:

now

assume A14: p is not Element of AS ; :: thesis:

now

A15: b <> d by A2, A4, A5, A6, A9, A12, A13, Lm2;
consider x being Element of AS;
assume that
A16: a is not Element of AS and
A17: b is not Element of AS and
A18: c is not Element of AS and
A19: d is not Element of AS ; :: thesis:
consider Xa being Subset of AS such that
A20: a = LDir Xa and
A21: Xa is being_line by A16, Th20;
consider Xc being Subset of AS such that
A22: c = LDir Xc and
A23: Xc is being_line by A18, Th20;
consider Xb being Subset of AS such that
A24: b = LDir Xb and
A25: Xb is being_line by A17, Th20;
consider Xd being Subset of AS such that
A26: d = LDir Xd and
A27: Xd is being_line by A19, Th20;
consider Xp being Subset of AS such that
A28: p = LDir Xp and
A29: Xp is being_line by A14, Th20;
set Xa9 = x * Xa;
set Xb9 = x * Xb;
set Xc9 = x * Xc;
set Xd9 = x * Xd;
set Xp9 = x * Xp;
consider y being Element of AS such that
A30: x <> y and
A31: y in x * Xa by A21, AFF_1:32, AFF_4:27;
A32: Xp // x * Xp by A29, AFF_4:def 3;
consider t being Element of AS such that
A33: x <> t and
A34: t in x * Xc by A23, AFF_1:32, AFF_4:27;
set Y1 = y * (x * Xp);
set Y2 = t * (x * Xp);
A35: x * Xp is being_line by A29, AFF_4:27;
then A36: y * (x * Xp) is being_line by AFF_4:27;
A37: t * (x * Xp) is being_line by A35, AFF_4:27;
A38: Xb // x * Xb by A25, AFF_4:def 3;
A39: x * Xd is being_line by A27, AFF_4:27;
A40: Xd // x * Xd by A27, AFF_4:def 3;
A41: x in x * Xc by A23, AFF_4:def 3;
A42: x in x * Xb by A25, AFF_4:def 3;
A43: x * Xb is being_line by A25, AFF_4:27;
A44: x in x * Xd by A27, AFF_4:def 3;
then consider XQ being Subset of AS such that
A45: x * Xb c= XQ and
A46: x * Xd c= XQ and
A47: XQ is being_plane by A43, A39, A42, AFF_4:38;
A48: x * Xa is being_line by A21, AFF_4:27;
A49: x * Xp // t * (x * Xp) by A35, AFF_4:def 3;
A50: not x * Xd // t * (x * Xp)

proof

assume x * Xd // t * (x * Xp) ; :: thesis:
then Xd // t * (x * Xp) by A40, AFF_1:58;
then Xd // x * Xp by A49, AFF_1:58;
then Xd // Xp by A32, AFF_1:58;
hence contradiction by A10, A12, A28, A29, A26, A27, Th11; :: thesis:

end;

A51: x * Xp // y * (x * Xp) by A35, AFF_4:def 3;
A52: not x * Xb // y * (x * Xp)

proof

assume x * Xb // y * (x * Xp) ; :: thesis:
then Xb // y * (x * Xp) by A38, AFF_1:58;
then Xb // x * Xp by A51, AFF_1:58;
then Xb // Xp by A32, AFF_1:58;
hence contradiction by A9, A12, A28, A29, A24, A25, Th11; :: thesis:

end;

A53: x in x * Xa by A21, AFF_4:def 3;
A54: x * Xc is being_line by A23, AFF_4:27;
then consider XP being Subset of AS such that
A55: x * Xa c= XP and
A56: x * Xc c= XP and
A57: XP is being_plane by A48, A53, A41, AFF_4:38;
A58: x in x * Xp by A29, AFF_4:def 3;
then consider X2 being Subset of AS such that
A59: x * Xc c= X2 and
A60: x * Xp c= X2 and
A61: X2 is being_plane by A54, A35, A41, AFF_4:38;
A62: Xc // x * Xc by A23, AFF_4:def 3;
N = [(PDir X2),2]

proof

reconsider N9 = [(PDir X2),2] as Element of the Lines of (IncProjSp_of AS) by A61, Th23;
A63: c on N9 by A22, A62, A59, A61, Th32;
p on N9 by A28, A32, A60, A61, Th32;
hence N = [(PDir X2),2] by A3, A6, A8, A11, A63, Lm2; :: thesis:

end;

then Xd '||' X2 by A4, A26, A27, A61, Th29;
then A64: x * Xd c= X2 by A39, A41, A44, A40, A59, A61, AFF_4:43, AFF_4:56;
consider X1 being Subset of the carrier of AS such that
A65: x * Xa c= X1 and
A66: x * Xp c= X1 and
A67: X1 is being_plane by A48, A35, A53, A58, AFF_4:38;
A68: Xa // x * Xa by A21, AFF_4:def 3;
M = [(PDir X1),2]

proof

reconsider M9 = [(PDir X1),2] as Element of the Lines of (IncProjSp_of AS) by A67, Th23;
A69: a on M9 by A20, A68, A65, A67, Th32;
p on M9 by A28, A32, A66, A67, Th32;
hence M = [(PDir X1),2] by A1, A5, A7, A11, A69, Lm2; :: thesis:

end;

then Xb '||' X1 by A2, A24, A25, A67, Th29;
then A70: x * Xb c= X1 by A43, A53, A42, A38, A65, A67, AFF_4:43, AFF_4:56;
y * (x * Xp) c= X1 by A29, A31, A65, A66, A67, AFF_4:27, AFF_4:28;
then consider z being Element of AS such that
A71: z in x * Xb and
A72: z in y * (x * Xp) by A43, A36, A67, A70, A52, AFF_4:22;
t * (x * Xp) c= X2 by A29, A34, A59, A60, A61, AFF_4:27, AFF_4:28;
then consider u being Element of AS such that
A73: u in x * Xd and
A74: u in t * (x * Xp) by A39, A37, A61, A64, A50, AFF_4:22;
set AC = Line (y,t);
set BD = Line (z,u);
A75: y in Line (y,t) by AFF_1:26;
A76: y in y * (x * Xp) by A35, AFF_4:def 3;
A77: x <> z

proof

assume A78: not x <> z ; :: thesis:
a = LDir (x * Xa) by A20, A21, A48, A68, Th11
.= LDir (y * (x * Xp)) by A48, A53, A30, A31, A36, A76, A72, A78, AFF_1:30
.= LDir (x * Xp) by A35, A36, A51, Th11
.= p by A28, A29, A35, A32, Th11 ;
hence contradiction by A7, A11; :: thesis:

end;

A79: z <> u

proof

assume A80: not z <> u ; :: thesis:
b = LDir (x * Xb) by A24, A25, A43, A38, Th11
.= LDir (x * Xd) by A43, A39, A42, A44, A71, A73, A77, A80, AFF_1:30
.= d by A26, A27, A39, A40, Th11 ;
hence contradiction by A2, A4, A5, A6, A9, A12, A13, Lm2; :: thesis:

end;

then A81: Line (z,u) is being_line by AFF_1:def 3;
A82: x * Xa <> x * Xc

proof

assume x * Xa = x * Xc ; :: thesis:
then a = LDir (x * Xc) by A20, A21, A48, A68, Th11
.= c by A22, A23, A54, A62, Th11 ;
hence contradiction by A1, A3, A5, A6, A7, A11, A13, Lm2; :: thesis:

end;

then A83: y <> t by A48, A54, A53, A41, A30, A31, A34, AFF_1:30;
then A84: Line (y,t) is being_line by AFF_1:def 3;
A85: Line (z,u) c= XQ by A71, A73, A79, A45, A46, A47, AFF_4:19;
A86: t in Line (y,t) by AFF_1:26;
y * (x * Xp) // t * (x * Xp) by A51, A49, AFF_1:58;
then consider X3 being Subset of AS such that
A87: y * (x * Xp) c= X3 and
A88: t * (x * Xp) c= X3 and
A89: X3 is being_plane by AFF_4:39;
A90: Line (z,u) c= X3 by A87, A88, A89, A72, A74, A79, AFF_4:19;
A91: a <> c by A1, A3, A5, A6, A7, A11, A13, Lm2;
A92: ( P = [(PDir XP),2] & Q = [(PDir XQ),2] )

proof

reconsider P9 = [(PDir XP),2], Q9 = [(PDir XQ),2] as LINE of (IncProjSp_of AS) by A57, A47, Th23;
A93: c on P9 by A22, A62, A56, A57, Th32;
A94: b on Q9 by A24, A38, A45, A47, Th32;
A95: d on Q9 by A26, A40, A46, A47, Th32;
a on P9 by A20, A68, A55, A57, Th32;
hence ( P = [(PDir XP),2] & Q = [(PDir XQ),2] ) by A7, A8, A9, A10, A91, A15, A93, A94, A95, Lm2; :: thesis:

end;

A96: now

reconsider q = LDir (Line (y,t)), q9 = LDir (Line (z,u)) as Element of the Points of (IncProjSp_of AS) by A84, A81, Th20;
assume A97: Line (y,t) // Line (z,u) ; :: thesis:
take q = q; :: thesis:
q = q9 by A84, A81, A97, Th11;
hence ( q on P & q on Q ) by A31, A34, A71, A73, A83, A79, A84, A81, A55, A56, A57, A45, A46, A47, A92, Th31, AFF_4:19; :: thesis:

end;

A98: Line (y,t) c= XP by A31, A34, A83, A55, A56, A57, AFF_4:19;

A99: now

given w being Element of AS such that A100: w in Line (y,t) and
A101: w in Line (z,u) ; :: thesis:
set R = Line (x,w);
A102: x <> w

proof

assume A103: x = w ; :: thesis:
then x * Xa = Line (y,t) by A48, A53, A30, A31, A84, A75, A100, AFF_1:30;
hence contradiction by A54, A41, A33, A34, A82, A84, A86, A100, A103, AFF_1:30; :: thesis:

end;

then A104: Line (x,w) is being_line by AFF_1:def 3;
then reconsider q = LDir (Line (x,w)) as POINT of (IncProjSp_of AS) by Th20;
take q = q; :: thesis:
thus ( q on P & q on Q ) by A53, A42, A55, A57, A45, A47, A92, A98, A85, A100, A101, A102, A104, Th31, AFF_4:19; :: thesis:

end;

t in t * (x * Xp) by A35, AFF_4:def 3;
then Line (y,t) c= X3 by A76, A87, A88, A89, A83, AFF_4:19;
hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A89, A84, A81, A90, A96, A99, AFF_4:22; :: thesis:

end;

hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, Lm11; :: thesis:

end;

hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, Lm9; :: thesis: