let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for a, b, c, d, p, pp9, q being POINT of IPP

for O1, O2, O3, A, B, C, O, Q being LINE of IPP st not a on A & not a on C & not b on C & not b on Q & not A,B,C are_concurrent & not B,C,O are_concurrent & A <> Q & Q <> C & a <> b & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on O2 & {b,d,pp9} on O3 holds

( q <> a & q <> b & not q on A & not q on Q )

let a, b, c, d, p, pp9, q be POINT of IPP; :: thesis: for O1, O2, O3, A, B, C, O, Q being LINE of IPP st not a on A & not a on C & not b on C & not b on Q & not A,B,C are_concurrent & not B,C,O are_concurrent & A <> Q & Q <> C & a <> b & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on O2 & {b,d,pp9} on O3 holds

( q <> a & q <> b & not q on A & not q on Q )

let O1, O2, O3, A, B, C, O, Q be LINE of IPP; :: thesis: ( not a on A & not a on C & not b on C & not b on Q & not A,B,C are_concurrent & not B,C,O are_concurrent & A <> Q & Q <> C & a <> b & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on O2 & {b,d,pp9} on O3 implies ( q <> a & q <> b & not q on A & not q on Q ) )

assume that

A1: not a on A and

A2: not a on C and

A3: not b on C and

A4: not b on Q and

A5: not A,B,C are_concurrent and

A6: not B,C,O are_concurrent and

A7: A <> Q and

A8: Q <> C and

A9: a <> b and

A10: {c,p} on A and

A11: d on B and

A12: {c,d} on C and

A13: {a,b,q} on O and

A14: {c,pp9} on Q and

A15: {a,d,p} on O1 and

A16: {q,p,pp9} on O2 and

A17: {b,d,pp9} on O3 ; :: thesis: ( q <> a & q <> b & not q on A & not q on Q )

A18: d on C by A12, INCSP_1:1;

A19: c on C by A12, INCSP_1:1;

A20: c on A by A10, INCSP_1:1;

then A21: c <> d by A5, A11, A19;

A22: d on O1 by A15, INCSP_1:2;

A23: pp9 on Q by A14, INCSP_1:1;

A24: pp9 on O3 by A17, INCSP_1:2;

A25: pp9 on O2 by A16, INCSP_1:2;

A26: a on O1 by A15, INCSP_1:2;

A27: b on O3 by A17, INCSP_1:2;

A28: d on O3 by A17, INCSP_1:2;

A29: q on O by A13, INCSP_1:2;

A30: b on O by A13, INCSP_1:2;

A31: q <> pp9

A33: ( pp9 on Q & p on O2 ) by A14, A16, INCSP_1:1, INCSP_1:2;

A34: p on A by A10, INCSP_1:1;

A35: c on Q by A14, INCSP_1:1;

then A36: pp9 <> d by A8, A19, A18, A23, A21, INCPROJ:def 4;

A37: O1 <> O2

then A40: p <> c by A2, A19, A18, A26, A22, A21, INCPROJ:def 4;

A41: not q on Q

A43: q <> p

pp9 <> c by A3, A19, A18, A28, A27, A24, A21, INCPROJ:def 4;

then A45: A <> O2 by A7, A20, A35, A25, A23, INCPROJ:def 4;

A46: q on O2 by A16, INCSP_1:2;

A47: p <> d by A5, A11, A18, A34;

q <> b

for O1, O2, O3, A, B, C, O, Q being LINE of IPP st not a on A & not a on C & not b on C & not b on Q & not A,B,C are_concurrent & not B,C,O are_concurrent & A <> Q & Q <> C & a <> b & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on O2 & {b,d,pp9} on O3 holds

( q <> a & q <> b & not q on A & not q on Q )

let a, b, c, d, p, pp9, q be POINT of IPP; :: thesis: for O1, O2, O3, A, B, C, O, Q being LINE of IPP st not a on A & not a on C & not b on C & not b on Q & not A,B,C are_concurrent & not B,C,O are_concurrent & A <> Q & Q <> C & a <> b & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on O2 & {b,d,pp9} on O3 holds

( q <> a & q <> b & not q on A & not q on Q )

let O1, O2, O3, A, B, C, O, Q be LINE of IPP; :: thesis: ( not a on A & not a on C & not b on C & not b on Q & not A,B,C are_concurrent & not B,C,O are_concurrent & A <> Q & Q <> C & a <> b & {c,p} on A & d on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on O2 & {b,d,pp9} on O3 implies ( q <> a & q <> b & not q on A & not q on Q ) )

assume that

A1: not a on A and

A2: not a on C and

A3: not b on C and

A4: not b on Q and

A5: not A,B,C are_concurrent and

A6: not B,C,O are_concurrent and

A7: A <> Q and

A8: Q <> C and

A9: a <> b and

A10: {c,p} on A and

A11: d on B and

A12: {c,d} on C and

A13: {a,b,q} on O and

A14: {c,pp9} on Q and

A15: {a,d,p} on O1 and

A16: {q,p,pp9} on O2 and

A17: {b,d,pp9} on O3 ; :: thesis: ( q <> a & q <> b & not q on A & not q on Q )

A18: d on C by A12, INCSP_1:1;

A19: c on C by A12, INCSP_1:1;

A20: c on A by A10, INCSP_1:1;

then A21: c <> d by A5, A11, A19;

A22: d on O1 by A15, INCSP_1:2;

A23: pp9 on Q by A14, INCSP_1:1;

A24: pp9 on O3 by A17, INCSP_1:2;

A25: pp9 on O2 by A16, INCSP_1:2;

A26: a on O1 by A15, INCSP_1:2;

A27: b on O3 by A17, INCSP_1:2;

A28: d on O3 by A17, INCSP_1:2;

A29: q on O by A13, INCSP_1:2;

A30: b on O by A13, INCSP_1:2;

A31: q <> pp9

proof

A32:
( pp9 on O2 & q on O2 )
by A16, INCSP_1:2;
assume
not q <> pp9
; :: thesis: contradiction

then O3 = O by A4, A30, A29, A27, A24, A23, INCPROJ:def 4;

hence contradiction by A6, A11, A18, A28; :: thesis: verum

end;then O3 = O by A4, A30, A29, A27, A24, A23, INCPROJ:def 4;

hence contradiction by A6, A11, A18, A28; :: thesis: verum

A33: ( pp9 on Q & p on O2 ) by A14, A16, INCSP_1:1, INCSP_1:2;

A34: p on A by A10, INCSP_1:1;

A35: c on Q by A14, INCSP_1:1;

then A36: pp9 <> d by A8, A19, A18, A23, A21, INCPROJ:def 4;

A37: O1 <> O2

proof

A39:
p on O1
by A15, INCSP_1:2;
assume
not O1 <> O2
; :: thesis: contradiction

then A38: a on O3 by A26, A22, A25, A28, A24, A36, INCPROJ:def 4;

( a on O & b on O ) by A13, INCSP_1:2;

then d on O by A9, A28, A27, A38, INCPROJ:def 4;

hence contradiction by A6, A11, A18; :: thesis: verum

end;then A38: a on O3 by A26, A22, A25, A28, A24, A36, INCPROJ:def 4;

( a on O & b on O ) by A13, INCSP_1:2;

then d on O by A9, A28, A27, A38, INCPROJ:def 4;

hence contradiction by A6, A11, A18; :: thesis: verum

then A40: p <> c by A2, A19, A18, A26, A22, A21, INCPROJ:def 4;

A41: not q on Q

proof

A42:
a on O
by A13, INCSP_1:2;
assume
q on Q
; :: thesis: contradiction

then p on Q by A33, A32, A31, INCPROJ:def 4;

hence contradiction by A7, A20, A35, A34, A40, INCPROJ:def 4; :: thesis: verum

end;then p on Q by A33, A32, A31, INCPROJ:def 4;

hence contradiction by A7, A20, A35, A34, A40, INCPROJ:def 4; :: thesis: verum

A43: q <> p

proof

A44:
p on O2
by A16, INCSP_1:2;
assume
not q <> p
; :: thesis: contradiction

then O = O1 by A1, A42, A26, A34, A39, A29, INCPROJ:def 4;

hence contradiction by A6, A11, A18, A22; :: thesis: verum

end;then O = O1 by A1, A42, A26, A34, A39, A29, INCPROJ:def 4;

hence contradiction by A6, A11, A18, A22; :: thesis: verum

pp9 <> c by A3, A19, A18, A28, A27, A24, A21, INCPROJ:def 4;

then A45: A <> O2 by A7, A20, A35, A25, A23, INCPROJ:def 4;

A46: q on O2 by A16, INCSP_1:2;

A47: p <> d by A5, A11, A18, A34;

q <> b

proof

hence
( q <> a & q <> b & not q on A & not q on Q )
by A26, A34, A39, A46, A44, A45, A37, A43, A41, INCPROJ:def 4; :: thesis: verum
assume
not q <> b
; :: thesis: contradiction

then O2 = O3 by A4, A46, A25, A27, A24, A23, INCPROJ:def 4;

hence contradiction by A22, A39, A44, A28, A47, A37, INCPROJ:def 4; :: thesis: verum

end;then O2 = O3 by A4, A46, A25, A27, A24, A23, INCPROJ:def 4;

hence contradiction by A22, A39, A44, A28, A47, A37, INCPROJ:def 4; :: thesis: verum