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 & 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 ) and
A2: ( not p on P & not p on Q ) and
A3: M <> N ; :: thesis:

now

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

now

assume A5: ( a is not Element of AS & b is not Element of AS & c is not Element of AS & d is not Element of AS ) ; :: thesis:
consider Xp being Subset of AS such that
A6: ( p = LDir Xp & Xp is being_line ) by A4, Th20;
consider Xa being Subset of AS such that
A7: ( a = LDir Xa & Xa is being_line ) by A5, Th20;
consider Xb being Subset of AS such that
A8: ( b = LDir Xb & Xb is being_line ) by A5, Th20;
consider Xc being Subset of AS such that
A9: ( c = LDir Xc & Xc is being_line ) by A5, Th20;
consider Xd being Subset of AS such that
A10: ( d = LDir Xd & Xd is being_line ) by A5, Th20;
A11: ( a <> c & b <> d ) by A1, A2, A3, Lm2;
consider x being Element of AS;
set Xa' = x * Xa;
set Xb' = x * Xb;
set Xc' = x * Xc;
set Xd' = x * Xd;
set Xp' = x * Xp;
A12: ( x * Xa is being_line & x * Xb is being_line & x * Xc is being_line & x * Xd is being_line & x * Xp is being_line & x in x * Xa & x in x * Xb & x in x * Xc & x in x * Xd & x in x * Xp & Xa // x * Xa & Xb // x * Xb & Xc // x * Xc & Xd // x * Xd & Xp // x * Xp ) by A6, A7, A8, A9, A10, AFF_4:27, AFF_4:def 3;
then consider y being Element of AS such that
A13: ( x <> y & y in x * Xa ) by AFF_1:32;
consider t being Element of AS such that
A14: ( x <> t & t in x * Xc ) by A12, AFF_1:32;
set Y1 = y * (x * Xp);
set Y2 = t * (x * Xp);
A15: ( y * (x * Xp) is being_line & t * (x * Xp) is being_line & y in y * (x * Xp) & t in t * (x * Xp) & x * Xp // y * (x * Xp) & x * Xp // t * (x * Xp) ) by A12, AFF_4:27, AFF_4:def 3;
then A16: y * (x * Xp) // t * (x * Xp) by AFF_1:58;
consider X1 being Subset of the carrier of AS such that
A17: ( x * Xa c= X1 & x * Xp c= X1 & X1 is being_plane ) by A12, AFF_4:38;
consider X2 being Subset of AS such that
A18: ( x * Xc c= X2 & x * Xp c= X2 & X2 is being_plane ) by A12, AFF_4:38;
consider X3 being Subset of AS such that
A19: ( y * (x * Xp) c= X3 & t * (x * Xp) c= X3 & X3 is being_plane ) by A16, AFF_4:39;
A20: ( y * (x * Xp) c= X1 & t * (x * Xp) c= X2 ) by A12, A13, A14, A17, A18, AFF_4:28;
A21: M = [(PDir X1),2]

proof

reconsider M' = [(PDir X1),2] as Element of the Lines of (IncProjSp_of AS) by A17, Th23;
( p on M' & a on M' ) by A6, A7, A12, A17, Th32;
hence M = [(PDir X1),2] by A1, A2, Lm2; :: thesis:

end;

A22: N = [(PDir X2),2]

proof

reconsider N' = [(PDir X2),2] as Element of the Lines of (IncProjSp_of AS) by A18, Th23;
( p on N' & c on N' ) by A6, A9, A12, A18, Th32;
hence N = [(PDir X2),2] by A1, A2, Lm2; :: thesis:

end;

A23: ( x * Xb c= X1 & x * Xd c= X2 )

proof

( Xb '||' X1 & Xd '||' X2 ) by A1, A8, A10, A17, A18, A21, A22, Th29;
hence ( x * Xb c= X1 & x * Xd c= X2 ) by A12, A17, A18, AFF_4:43, AFF_4:56; :: thesis:

end;

A24: not x * Xb // y * (x * Xp)

proof

assume x * Xb // y * (x * Xp) ; :: thesis:
then Xb // y * (x * Xp) by A12, AFF_1:58;
then Xb // x * Xp by A15, AFF_1:58;
then Xb // Xp by A12, AFF_1:58;
hence contradiction by A1, A2, A6, A8, Th11; :: thesis:

end;

A25: not x * Xd // t * (x * Xp)

proof

assume x * Xd // t * (x * Xp) ; :: thesis:
then Xd // t * (x * Xp) by A12, AFF_1:58;
then Xd // x * Xp by A15, AFF_1:58;
then Xd // Xp by A12, AFF_1:58;
hence contradiction by A1, A2, A6, A10, Th11; :: thesis:

end;

consider z being Element of AS such that
A26: ( z in x * Xb & z in y * (x * Xp) ) by A12, A15, A17, A20, A23, A24, AFF_4:22;
consider u being Element of AS such that
A27: ( u in x * Xd & u in t * (x * Xp) ) by A12, A15, A18, A20, A23, A25, AFF_4:22;
set AC = Line y,t;
set BD = Line z,u;
A28: x * Xa <> x * Xc

proof

assume x * Xa = x * Xc ; :: thesis:
then a = LDir (x * Xc) by A7, A12, Th11
.= c by A9, A12, Th11 ;
hence contradiction by A1, A2, A3, Lm2; :: thesis:

end;

then A29: y <> t by A12, A13, A14, AFF_1:30;
A30: x <> z

proof

assume A31: not x <> z ; :: thesis:
a = LDir (x * Xa) by A7, A12, Th11
.= LDir (y * (x * Xp)) by A12, A13, A15, A26, A31, AFF_1:30
.= LDir (x * Xp) by A12, A15, Th11
.= p by A6, A12, Th11 ;
hence contradiction by A1, A2; :: thesis:

end;

A32: z <> u

proof

assume A33: not z <> u ; :: thesis:
b = LDir (x * Xb) by A8, A12, Th11
.= LDir (x * Xd) by A12, A26, A27, A30, A33, AFF_1:30
.= d by A10, A12, Th11 ;
hence contradiction by A1, A2, A3, Lm2; :: thesis:

end;

then A34: ( Line y,t is being_line & Line z,u is being_line ) by A29, AFF_1:def 3;
A35: ( Line y,t c= X3 & Line z,u c= X3 ) by A15, A19, A26, A27, A29, A32, AFF_4:19;
consider XP being Subset of AS such that
A36: ( x * Xa c= XP & x * Xc c= XP & XP is being_plane ) by A12, AFF_4:38;
consider XQ being Subset of AS such that
A37: ( x * Xb c= XQ & x * Xd c= XQ & XQ is being_plane ) by A12, AFF_4:38;
A38: ( y in Line y,t & t in Line y,t ) by AFF_1:26;
A39: ( P = [(PDir XP),2] & Q = [(PDir XQ),2] )

proof

reconsider P' = [(PDir XP),2], Q' = [(PDir XQ),2] as LINE of (IncProjSp_of AS) by A36, A37, Th23;
( a on P' & c on P' & b on Q' & d on Q' ) by A7, A8, A9, A10, A12, A36, A37, Th32;
hence ( P = [(PDir XP),2] & Q = [(PDir XQ),2] ) by A1, A11, Lm2; :: thesis:

end;

A40: ( Line y,t c= XP & Line z,u c= XQ ) by A13, A14, A26, A27, A29, A32, A36, A37, AFF_4:19;

A41: now

assume A42: Line y,t // Line z,u ; :: thesis:
reconsider q = LDir (Line y,t), q' = LDir (Line z,u) as Element of the Points of (IncProjSp_of AS) by A34, Th20;
take q = q; :: thesis:
q = q' by A34, A42, Th11;
hence ( q on P & q on Q ) by A13, A14, A26, A27, A29, A32, A34, A36, A37, A39, Th31, AFF_4:19; :: thesis:

end;

now

given w being Element of AS such that A43: ( w in Line y,t & w in Line z,u ) ; :: thesis:
A44: x <> w

proof

assume x = w ; :: thesis:
then ( x * Xa = Line y,t & x * Xc = Line y,t ) by A12, A13, A14, A34, A38, A43, AFF_1:30;
hence contradiction by A28; :: thesis:

end;

set R = Line x,w;
A45: Line x,w is being_line by A44, 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 A12, A36, A37, A39, A40, A43, A44, A45, Th31, AFF_4:19; :: thesis:

end;

hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A19, A34, A35, A41, 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, Lm11; :: thesis:

end;

hence ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by A1, A2, A3, Lm9; :: thesis: