let PCPP be Pappian CollProjectivePlane; :: thesis: for o, b1, a1, b2, a2, b3, a3, c1, c3, c2 being Element of PCPP st o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & not o,c1,c3 is_collinear & a1,a2,c3 is_collinear & b1,b2,c3 is_collinear & a2,a3,c1 is_collinear & b2,b3,c1 is_collinear & a1,a3,c2 is_collinear & b1,b3,c2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear holds
c1,c2,c3 is_collinear
let o, b1, a1, b2, a2, b3, a3, c1, c3, c2 be Element of PCPP; :: thesis: ( o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & not o,c1,c3 is_collinear & a1,a2,c3 is_collinear & b1,b2,c3 is_collinear & a2,a3,c1 is_collinear & b2,b3,c1 is_collinear & a1,a3,c2 is_collinear & b1,b3,c2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear implies c1,c2,c3 is_collinear )
assume that
A1:
( o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 )
and
A2:
( not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear )
and
A3:
not o,c1,c3 is_collinear
and
A4:
( a1,a2,c3 is_collinear & b1,b2,c3 is_collinear & a2,a3,c1 is_collinear & b2,b3,c1 is_collinear & a1,a3,c2 is_collinear & b1,b3,c2 is_collinear )
and
A5:
( o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear )
; :: thesis: c1,c2,c3 is_collinear
A6:
( o <> a1 & o <> a2 & a1 <> a2 & o <> a3 & a1 <> a3 & a2 <> a3 )
by A2, ANPROJ_2:def 7;
now assume A7:
( not
a1,
a2,
a3 is_collinear & not
b1,
b2,
b3 is_collinear )
;
:: thesis: ( not c1,c2,c3 is_collinear implies c1,c2,c3 is_collinear )consider x being
Element of
PCPP such that A8:
(
a1,
a3,
x is_collinear &
o,
a2,
x is_collinear )
by ANPROJ_2:def 14;
consider y being
Element of
PCPP such that A9:
(
b1,
b3,
y is_collinear &
o,
a2,
y is_collinear )
by ANPROJ_2:def 14;
consider a being
Element of
PCPP such that A10:
(
o,
a2,
a is_collinear &
c1,
c3,
a is_collinear )
by ANPROJ_2:def 14;
consider z being
Element of
PCPP such that A11:
(
a1,
a3,
z is_collinear &
c1,
c3,
z is_collinear )
by ANPROJ_2:def 14;
assume A12:
not
c1,
c2,
c3 is_collinear
;
:: thesis: c1,c2,c3 is_collinear A13:
now assume A14:
(
c1,
c3,
x is_collinear &
c1,
c3,
y is_collinear )
;
:: thesis: contradictionthus
contradiction
:: thesis: verumproof
A15:
(
a1 <> c3 &
a2 <> c3 &
a2 <> c1 &
a3 <> c1 &
c1 <> c3 )
proof
A16:
a1 <> c3
proof
( not
o,
a2,
a1 is_collinear &
a2,
a1,
c3 is_collinear &
b2,
b1,
c3 is_collinear )
by A2, A4, Th3;
hence
a1 <> c3
by A1, A5, Th10;
:: thesis: verum
end;
( not
o,
a3,
a2 is_collinear &
b3,
b2,
c1 is_collinear &
a3,
a2,
c1 is_collinear )
by A2, A4, Th3;
hence
(
a1 <> c3 &
a2 <> c3 &
a2 <> c1 &
a3 <> c1 &
c1 <> c3 )
by A1, A2, A3, A4, A5, A16, Th10, ANPROJ_2:def 7;
:: thesis: verum
end;
A17:
(
o <> a &
a2 <> a &
o <> a2 &
a1 <> a3 &
a1 <> z &
a3 <> z )
proof
A18:
a2 <> c3
by A1, A2, A4, A5, Th10;
A19:
c1 <> c3
by A3, ANPROJ_2:def 7;
( not
o,
a3,
a2 is_collinear &
b3,
b2,
c1 is_collinear &
a3,
a2,
c1 is_collinear )
by A2, A4, Th3;
then A20:
a2 <> c1
by A1, A5, Th10;
A21:
a2 <> a
proof
assume A22:
not
a2 <> a
;
:: thesis: contradiction
then
(
c3,
a2,
c1 is_collinear &
c3,
a2,
a1 is_collinear &
c1,
a2,
c3 is_collinear &
c1,
a2,
a3 is_collinear )
by A4, A10, Th3;
then
(
c3,
c1,
a1 is_collinear &
c1,
c3,
a3 is_collinear )
by A18, A20, Th4;
then
(
c1,
c3,
a1 is_collinear &
c1,
c3,
a3 is_collinear )
by Th3;
hence
contradiction
by A7, A10, A19, A22, ANPROJ_2:def 8;
:: thesis: verum
end;
A23:
a1 <> c3
proof
( not
o,
a2,
a1 is_collinear &
a2,
a1,
c3 is_collinear &
b2,
b1,
c3 is_collinear )
by A2, A4, Th3;
hence
a1 <> c3
by A1, A5, Th10;
:: thesis: verum
end;
a3 <> c1
by A1, A2, A4, A5, Th10;
hence
(
o <> a &
a2 <> a &
o <> a2 &
a1 <> a3 &
a1 <> z &
a3 <> z )
by A2, A3, A4, A7, A10, A11, A18, A20, A21, A23, Th3, Th12, ANPROJ_2:def 7;
:: thesis: verum
end;
A24:
not
o,
a2,
c1 is_collinear
proof
( not
a2,
a3,
o is_collinear &
a2,
a3,
c1 is_collinear &
a2 <> c1 )
by A2, A4, A15, Th3;
then
not
a2,
c1,
o is_collinear
by Th8;
hence
not
o,
a2,
c1 is_collinear
by Th3;
:: thesis: verum
end;
A25:
(
b1 <> b2 &
b1 <> b3 &
b2 <> b3 )
by A1, A2, A5, Th9;
A26:
b1,
b3,
x is_collinear
by A8, A9, A14, A15, A17, A24, Th17;
( not
a1,
o,
a3 is_collinear &
a1,
o,
b1 is_collinear &
a1 <> b1 )
by A1, A2, A5, Th3;
then
not
a1,
b1,
a3 is_collinear
by Th8;
then
not
a1,
a3,
b1 is_collinear
by Th3;
then
c1,
c3,
c2 is_collinear
by A4, A6, A8, A14, A25, A26, Th17;
hence
contradiction
by A12, Th3;
:: thesis: verum
end; end; now assume A27:
( not
c1,
c3,
x is_collinear or not
c1,
c3,
y is_collinear )
;
:: thesis: c1,c2,c3 is_collinear now assume A28:
not
c1,
c3,
y is_collinear
;
:: thesis: contradictionA29:
o,
b2,
y is_collinear
by A5, A6, A9, Th4;
A30:
(
o,
b1,
a1 is_collinear &
o,
b2,
a2 is_collinear &
o,
b3,
a3 is_collinear )
by A5, Th3;
( not
o,
b1,
b2 is_collinear & not
o,
b2,
b3 is_collinear & not
o,
b1,
b3 is_collinear )
by A1, A2, A5, Th19;
hence
contradiction
by A1, A3, A4, A6, A9, A12, A28, A29, A30, Lm2;
:: thesis: verum end; hence
c1,
c2,
c3 is_collinear
by A1, A2, A3, A4, A5, A8, A27, Lm2;
:: thesis: verum end; hence
c1,
c2,
c3 is_collinear
by A13;
:: thesis: verum end;
hence
c1,c2,c3 is_collinear
by A1, A2, A3, A4, A5, Lm1; :: thesis: verum