let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for a, b, c, d, q, o, o9, o99, oo9 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 B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & A <> Q & {c,o} on A & {o,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O holds

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

let a, b, c, d, q, o, o9, o99, oo9 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 B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & A <> Q & {c,o} on A & {o,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O holds

( not q on A & not q on Q & b <> 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 B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & A <> Q & {c,o} on A & {o,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O implies ( not q on A & not q on Q & b <> q ) )

assume that

A1: not a on A and

A2: not a on C and

A3: not b on B and

A4: not b on C and

A5: not b on Q and

A6: not A,B,C are_concurrent and

A7: a <> b and

A8: A <> Q and

A9: {c,o} on A and

A10: {o,o99,d} on B and

A11: {c,d,o9} on C and

A12: {a,b,d} on O and

A13: {c,oo9} on Q and

A14: {a,o,o9} on O1 and

A15: {b,o9,oo9} on O2 and

A16: {o,oo9,q} on O3 and

A17: q on O ; :: thesis: ( not q on A & not q on Q & b <> q )

A18: o on B by A10, INCSP_1:2;

A19: ( c on A & c on Q ) by A9, A13, INCSP_1:1;

A20: o on A by A9, INCSP_1:1;

A21: oo9 on O2 by A15, INCSP_1:2;

A22: ( b on O2 & oo9 on O2 ) by A15, INCSP_1:2;

A23: oo9 on Q by A13, INCSP_1:1;

A24: b on O2 by A15, INCSP_1:2;

A25: o on O1 by A14, INCSP_1:2;

A26: o on A by A9, INCSP_1:1;

A27: d on C by A11, INCSP_1:2;

then A28: o <> d by A6, A26, A18;

A29: d on B by A10, INCSP_1:2;

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

A31: oo9 on Q by A13, INCSP_1:1;

A32: o9 on O2 by A15, INCSP_1:2;

A33: q on O3 by A16, INCSP_1:2;

A34: a on O1 by A14, INCSP_1:2;

A35: d on O by A12, INCSP_1:2;

A36: a on O by A12, INCSP_1:2;

A37: O1 <> O2

A39: o9 on C by A11, INCSP_1:2;

then A40: o <> o9 by A6, A26, A18;

A41: b <> q

A45: c on C by A11, INCSP_1:2;

then A46: o <> c by A6, A44, A18;

A47: o9 on O1 by A14, INCSP_1:2;

then o9 <> c by A1, A44, A26, A34, A25, A46, INCPROJ:def 4;

then A48: c <> oo9 by A4, A45, A39, A24, A32, A21, INCPROJ:def 4;

o9 <> d

then A49: q <> oo9 by A5, A17, A30, A31, A24, A21, INCPROJ:def 4;

A50: c on Q by A13, INCSP_1:1;

A51: not q on Q

not q on A

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 B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & A <> Q & {c,o} on A & {o,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O holds

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

let a, b, c, d, q, o, o9, o99, oo9 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 B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & A <> Q & {c,o} on A & {o,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O holds

( not q on A & not q on Q & b <> 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 B & not b on C & not b on Q & not A,B,C are_concurrent & a <> b & A <> Q & {c,o} on A & {o,o99,d} on B & {c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9,q} on O3 & q on O implies ( not q on A & not q on Q & b <> q ) )

assume that

A1: not a on A and

A2: not a on C and

A3: not b on B and

A4: not b on C and

A5: not b on Q and

A6: not A,B,C are_concurrent and

A7: a <> b and

A8: A <> Q and

A9: {c,o} on A and

A10: {o,o99,d} on B and

A11: {c,d,o9} on C and

A12: {a,b,d} on O and

A13: {c,oo9} on Q and

A14: {a,o,o9} on O1 and

A15: {b,o9,oo9} on O2 and

A16: {o,oo9,q} on O3 and

A17: q on O ; :: thesis: ( not q on A & not q on Q & b <> q )

A18: o on B by A10, INCSP_1:2;

A19: ( c on A & c on Q ) by A9, A13, INCSP_1:1;

A20: o on A by A9, INCSP_1:1;

A21: oo9 on O2 by A15, INCSP_1:2;

A22: ( b on O2 & oo9 on O2 ) by A15, INCSP_1:2;

A23: oo9 on Q by A13, INCSP_1:1;

A24: b on O2 by A15, INCSP_1:2;

A25: o on O1 by A14, INCSP_1:2;

A26: o on A by A9, INCSP_1:1;

A27: d on C by A11, INCSP_1:2;

then A28: o <> d by A6, A26, A18;

A29: d on B by A10, INCSP_1:2;

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

A31: oo9 on Q by A13, INCSP_1:1;

A32: o9 on O2 by A15, INCSP_1:2;

A33: q on O3 by A16, INCSP_1:2;

A34: a on O1 by A14, INCSP_1:2;

A35: d on O by A12, INCSP_1:2;

A36: a on O by A12, INCSP_1:2;

A37: O1 <> O2

proof

A38:
( o on O3 & oo9 on O3 )
by A16, INCSP_1:2;
assume
not O1 <> O2
; :: thesis: contradiction

then o on O by A7, A36, A30, A34, A25, A24, INCPROJ:def 4;

hence contradiction by A3, A18, A29, A30, A35, A28, INCPROJ:def 4; :: thesis: verum

end;then o on O by A7, A36, A30, A34, A25, A24, INCPROJ:def 4;

hence contradiction by A3, A18, A29, A30, A35, A28, INCPROJ:def 4; :: thesis: verum

A39: o9 on C by A11, INCSP_1:2;

then A40: o <> o9 by A6, A26, A18;

A41: b <> q

proof

A44:
c on A
by A9, INCSP_1:1;
assume
not b <> q
; :: thesis: contradiction

then A42: o on O2 by A5, A23, A22, A38, A33, INCPROJ:def 4;

A43: o9 on O2 by A15, INCSP_1:2;

( o on O1 & o9 on O1 ) by A14, INCSP_1:2;

hence contradiction by A37, A40, A42, A43, INCPROJ:def 4; :: thesis: verum

end;then A42: o on O2 by A5, A23, A22, A38, A33, INCPROJ:def 4;

A43: o9 on O2 by A15, INCSP_1:2;

( o on O1 & o9 on O1 ) by A14, INCSP_1:2;

hence contradiction by A37, A40, A42, A43, INCPROJ:def 4; :: thesis: verum

A45: c on C by A11, INCSP_1:2;

then A46: o <> c by A6, A44, A18;

A47: o9 on O1 by A14, INCSP_1:2;

then o9 <> c by A1, A44, A26, A34, A25, A46, INCPROJ:def 4;

then A48: c <> oo9 by A4, A45, A39, A24, A32, A21, INCPROJ:def 4;

o9 <> d

proof

then
O <> O2
by A2, A27, A39, A36, A35, A32, INCPROJ:def 4;
assume
not o9 <> d
; :: thesis: contradiction

then O1 = O by A2, A27, A36, A35, A34, A47, INCPROJ:def 4;

hence contradiction by A3, A18, A29, A30, A35, A25, A28, INCPROJ:def 4; :: thesis: verum

end;then O1 = O by A2, A27, A36, A35, A34, A47, INCPROJ:def 4;

hence contradiction by A3, A18, A29, A30, A35, A25, A28, INCPROJ:def 4; :: thesis: verum

then A49: q <> oo9 by A5, A17, A30, A31, A24, A21, INCPROJ:def 4;

A50: c on Q by A13, INCSP_1:1;

A51: not q on Q

proof

A52:
q <> o
by A3, A17, A18, A29, A30, A35, A28, INCPROJ:def 4;
assume
q on Q
; :: thesis: contradiction

then o on Q by A23, A38, A33, A49, INCPROJ:def 4;

hence contradiction by A8, A44, A26, A50, A46, INCPROJ:def 4; :: thesis: verum

end;then o on Q by A23, A38, A33, A49, INCPROJ:def 4;

hence contradiction by A8, A44, A26, A50, A46, INCPROJ:def 4; :: thesis: verum

not q on A

proof

hence
( not q on A & not q on Q & b <> q )
by A51, A41; :: thesis: verum
assume
q on A
; :: thesis: contradiction

then oo9 on A by A20, A38, A33, A52, INCPROJ:def 4;

hence contradiction by A8, A19, A23, A48, INCPROJ:def 4; :: thesis: verum

end;then oo9 on A by A20, A38, A33, A52, INCPROJ:def 4;

hence contradiction by A8, A19, A23, A48, INCPROJ:def 4; :: thesis: verum