let c1, c2, c3, c4, c5, c6, c7, c8, c9, c10 be Element of (ProjectiveSpace (TOP-REAL 3)); ( c1 <> c2 & c1 <> c3 & c2 <> c3 & c2 <> c4 & c3 <> c4 & c1 <> c5 & c1 <> c6 & c5 <> c6 & c5 <> c7 & c6 <> c7 & not c1,c4,c7 are_collinear & c1,c4,c2 are_collinear & c1,c4,c3 are_collinear & c1,c7,c5 are_collinear & c1,c7,c6 are_collinear & c4,c5,c8 are_collinear & c7,c2,c8 are_collinear & c4,c6,c9 are_collinear & c3,c7,c9 are_collinear & c2,c6,c10 are_collinear & c3,c5,c10 are_collinear implies ( not c4,c2,c7 are_collinear & not c4,c3,c7 are_collinear & not c2,c3,c7 are_collinear & not c4,c2,c5 are_collinear & not c4,c2,c6 are_collinear & not c4,c3,c5 are_collinear & not c4,c3,c6 are_collinear & not c2,c7,c5 are_collinear & not c2,c7,c6 are_collinear & not c3,c7,c5 are_collinear & not c3,c7,c6 are_collinear & not c2,c3,c5 are_collinear & not c2,c3,c6 are_collinear & not c7,c5,c4 are_collinear & not c7,c6,c4 are_collinear & not c5,c6,c4 are_collinear & not c5,c6,c2 are_collinear & c4,c5,c8 are_collinear & c4,c6,c9 are_collinear & c2,c7,c8 are_collinear & c2,c6,c10 are_collinear & c3,c7,c9 are_collinear & c3,c5,c10 are_collinear ) )
assume that
A1:
c1 <> c2
and
A2:
c3 <> c1
and
A3:
c2 <> c3
and
A4:
c2 <> c4
and
A5:
c3 <> c4
and
A6:
c1 <> c5
and
A7:
c1 <> c6
and
A8:
c5 <> c6
and
A9:
c5 <> c7
and
A10:
c6 <> c7
and
A11:
not c1,c4,c7 are_collinear
and
A12:
c1,c4,c2 are_collinear
and
A13:
c1,c4,c3 are_collinear
and
A14:
c1,c7,c5 are_collinear
and
A15:
c1,c7,c6 are_collinear
and
A16:
c4,c5,c8 are_collinear
and
A17:
c7,c2,c8 are_collinear
and
A18:
c4,c6,c9 are_collinear
and
A19:
c3,c7,c9 are_collinear
and
A20:
c2,c6,c10 are_collinear
and
A21:
c3,c5,c10 are_collinear
; ( not c4,c2,c7 are_collinear & not c4,c3,c7 are_collinear & not c2,c3,c7 are_collinear & not c4,c2,c5 are_collinear & not c4,c2,c6 are_collinear & not c4,c3,c5 are_collinear & not c4,c3,c6 are_collinear & not c2,c7,c5 are_collinear & not c2,c7,c6 are_collinear & not c3,c7,c5 are_collinear & not c3,c7,c6 are_collinear & not c2,c3,c5 are_collinear & not c2,c3,c6 are_collinear & not c7,c5,c4 are_collinear & not c7,c6,c4 are_collinear & not c5,c6,c4 are_collinear & not c5,c6,c2 are_collinear & c4,c5,c8 are_collinear & c4,c6,c9 are_collinear & c2,c7,c8 are_collinear & c2,c6,c10 are_collinear & c3,c7,c9 are_collinear & c3,c5,c10 are_collinear )
assume A22:
( c4,c2,c7 are_collinear or c4,c3,c7 are_collinear or c2,c3,c7 are_collinear or c4,c2,c5 are_collinear or c4,c2,c6 are_collinear or c4,c3,c5 are_collinear or c4,c3,c6 are_collinear or c2,c7,c5 are_collinear or c2,c7,c6 are_collinear or c3,c7,c5 are_collinear or c3,c7,c6 are_collinear or c2,c3,c5 are_collinear or c2,c3,c6 are_collinear or c7,c5,c4 are_collinear or c7,c6,c4 are_collinear or c5,c6,c4 are_collinear or c5,c6,c2 are_collinear or not c4,c5,c8 are_collinear or not c4,c6,c9 are_collinear or not c2,c7,c8 are_collinear or not c2,c6,c10 are_collinear or not c3,c7,c9 are_collinear or not c3,c5,c10 are_collinear )
; contradiction
now ( not c1,c7,c4 are_collinear & c4,c2,c1 are_collinear & c4,c3,c1 are_collinear & not c2,c3,c7 are_collinear & c1,c5,c7 are_collinear & c7,c1,c5 are_collinear & c7,c6,c1 are_collinear & c1,c6,c7 are_collinear & c7,c1,c6 are_collinear & not c4,c3,c7 are_collinear & not c4,c2,c7 are_collinear & not c7,c1,c2 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c6 are_collinear or not c7,c6,v2 are_collinear or v100,c7,v2 are_collinear ) ) & ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c7,c7 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) ) & not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )thus
not
c1,
c7,
c4 are_collinear
by COLLSP:4, A11;
( c4,c2,c1 are_collinear & c4,c3,c1 are_collinear & not c2,c3,c7 are_collinear & c1,c5,c7 are_collinear & c7,c1,c5 are_collinear & c7,c6,c1 are_collinear & c1,c6,c7 are_collinear & c7,c1,c6 are_collinear & not c4,c3,c7 are_collinear & not c4,c2,c7 are_collinear & not c7,c1,c2 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c6 are_collinear or not c7,c6,v2 are_collinear or v100,c7,v2 are_collinear ) ) & ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c7,c7 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) ) & not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )thus
c4,
c2,
c1 are_collinear
by A12, HESSENBE:1;
( c4,c3,c1 are_collinear & not c2,c3,c7 are_collinear & c1,c5,c7 are_collinear & c7,c1,c5 are_collinear & c7,c6,c1 are_collinear & c1,c6,c7 are_collinear & c7,c1,c6 are_collinear & not c4,c3,c7 are_collinear & not c4,c2,c7 are_collinear & not c7,c1,c2 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c6 are_collinear or not c7,c6,v2 are_collinear or v100,c7,v2 are_collinear ) ) & ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c7,c7 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) ) & not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )thus
c4,
c3,
c1 are_collinear
by HESSENBE:1, A13;
( not c2,c3,c7 are_collinear & c1,c5,c7 are_collinear & c7,c1,c5 are_collinear & c7,c6,c1 are_collinear & c1,c6,c7 are_collinear & c7,c1,c6 are_collinear & not c4,c3,c7 are_collinear & not c4,c2,c7 are_collinear & not c7,c1,c2 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c6 are_collinear or not c7,c6,v2 are_collinear or v100,c7,v2 are_collinear ) ) & ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c7,c7 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) ) & not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )thus
not
c2,
c3,
c7 are_collinear
by A3, A11, A12, A13, HESSENBE:3;
( c1,c5,c7 are_collinear & c7,c1,c5 are_collinear & c7,c6,c1 are_collinear & c1,c6,c7 are_collinear & c7,c1,c6 are_collinear & not c4,c3,c7 are_collinear & not c4,c2,c7 are_collinear & not c7,c1,c2 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c6 are_collinear or not c7,c6,v2 are_collinear or v100,c7,v2 are_collinear ) ) & ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c7,c7 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) ) & not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )thus
c1,
c5,
c7 are_collinear
by A14, COLLSP:4;
( c7,c1,c5 are_collinear & c7,c6,c1 are_collinear & c1,c6,c7 are_collinear & c7,c1,c6 are_collinear & not c4,c3,c7 are_collinear & not c4,c2,c7 are_collinear & not c7,c1,c2 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c6 are_collinear or not c7,c6,v2 are_collinear or v100,c7,v2 are_collinear ) ) & ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c7,c7 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) ) & not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )thus
c7,
c1,
c5 are_collinear
by A14, COLLSP:4;
( c7,c6,c1 are_collinear & c1,c6,c7 are_collinear & c7,c1,c6 are_collinear & not c4,c3,c7 are_collinear & not c4,c2,c7 are_collinear & not c7,c1,c2 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c6 are_collinear or not c7,c6,v2 are_collinear or v100,c7,v2 are_collinear ) ) & ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c7,c7 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) ) & not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )thus
c7,
c6,
c1 are_collinear
by HESSENBE:1, A15;
( c1,c6,c7 are_collinear & c7,c1,c6 are_collinear & not c4,c3,c7 are_collinear & not c4,c2,c7 are_collinear & not c7,c1,c2 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c6 are_collinear or not c7,c6,v2 are_collinear or v100,c7,v2 are_collinear ) ) & ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c7,c7 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) ) & not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )thus
c1,
c6,
c7 are_collinear
by A15, COLLSP:4;
( c7,c1,c6 are_collinear & not c4,c3,c7 are_collinear & not c4,c2,c7 are_collinear & not c7,c1,c2 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c6 are_collinear or not c7,c6,v2 are_collinear or v100,c7,v2 are_collinear ) ) & ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c7,c7 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) ) & not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )thus
c7,
c1,
c6 are_collinear
by A15, COLLSP:4;
( not c4,c3,c7 are_collinear & not c4,c2,c7 are_collinear & not c7,c1,c2 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c6 are_collinear or not c7,c6,v2 are_collinear or v100,c7,v2 are_collinear ) ) & ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c7,c7 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) ) & not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )
( ( for
v100 being
Element of
(ProjectiveSpace (TOP-REAL 3)) holds
v100,
c4,
c4 are_collinear ) & ( for
v2,
v100 being
Element of
(ProjectiveSpace (TOP-REAL 3)) holds
( not
v100,
c4,
c4 are_collinear or not
v100,
c4,
c3 are_collinear or not
c4,
c3,
v2 are_collinear or
v100,
c4,
v2 are_collinear ) ) )
by COLLSP:2, A5, HESSENBE:3;
hence
not
c4,
c3,
c7 are_collinear
by A11, A13;
( not c4,c2,c7 are_collinear & not c7,c1,c2 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c6 are_collinear or not c7,c6,v2 are_collinear or v100,c7,v2 are_collinear ) ) & ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c7,c7 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) ) & not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )
( ( for
v100 being
Element of
(ProjectiveSpace (TOP-REAL 3)) holds
v100,
c4,
c4 are_collinear ) & ( for
v2,
v100 being
Element of
(ProjectiveSpace (TOP-REAL 3)) holds
( not
v100,
c4,
c4 are_collinear or not
v100,
c4,
c2 are_collinear or not
c4,
c2,
v2 are_collinear or
v100,
c4,
v2 are_collinear ) ) )
by COLLSP:2, A4, HESSENBE:3;
hence
not
c4,
c2,
c7 are_collinear
by A11, A12;
( not c7,c1,c2 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c6 are_collinear or not c7,c6,v2 are_collinear or v100,c7,v2 are_collinear ) ) & ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c7,c7 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) ) & not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )
( ( for
v100 being
Element of
(ProjectiveSpace (TOP-REAL 3)) holds
v100,
c1,
c1 are_collinear ) & ( for
v2,
v100 being
Element of
(ProjectiveSpace (TOP-REAL 3)) holds
( not
v100,
c1,
c1 are_collinear or not
v100,
c1,
c2 are_collinear or not
c1,
c2,
v2 are_collinear or
v100,
c1,
v2 are_collinear ) ) &
c1,
c2,
c4 are_collinear & not
c7,
c1,
c4 are_collinear )
by A12, COLLSP:2, A1, HESSENBE:1, HESSENBE:3, A11;
hence
not
c7,
c1,
c2 are_collinear
;
( ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c6 are_collinear or not c7,c6,v2 are_collinear or v100,c7,v2 are_collinear ) ) & ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c7,c7 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) ) & not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )thus
for
v2,
v100 being
Element of
(ProjectiveSpace (TOP-REAL 3)) holds
( not
v100,
c7,
c7 are_collinear or not
v100,
c7,
c6 are_collinear or not
c7,
c6,
v2 are_collinear or
v100,
c7,
v2 are_collinear )
by A10, HESSENBE:3;
( ( for v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds v100,c7,c7 are_collinear ) & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) ) & not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )thus
for
v100 being
Element of
(ProjectiveSpace (TOP-REAL 3)) holds
v100,
c7,
c7 are_collinear
by COLLSP:2;
( ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c7 are_collinear or not v100,c7,c5 are_collinear or not c7,c5,v2 are_collinear or v100,c7,v2 are_collinear ) ) & not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )thus
for
v2,
v100 being
Element of
(ProjectiveSpace (TOP-REAL 3)) holds
( not
v100,
c7,
c7 are_collinear or not
v100,
c7,
c5 are_collinear or not
c7,
c5,
v2 are_collinear or
v100,
c7,
v2 are_collinear )
by A9, HESSENBE:3;
( not c3,c7,c1 are_collinear & c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )now ( c3,c7,c7 are_collinear & not c3,c1,c7 are_collinear )thus
c3,
c7,
c7 are_collinear
by COLLSP:2;
not c3,c1,c7 are_collinear
c1,
c4,
c1 are_collinear
by COLLSP:2;
hence
not
c3,
c1,
c7 are_collinear
by A11, A2, A13, HESSENBE:3;
verum end; hence
not
c3,
c7,
c1 are_collinear
by HESSENBE:2, A11, A13;
( c5,c7,c1 are_collinear & not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )thus
c5,
c7,
c1 are_collinear
by HESSENBE:1, A14;
( not c2,c7,c1 are_collinear & c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )now ( c2,c7,c7 are_collinear & not c2,c1,c7 are_collinear )thus
c2,
c7,
c7 are_collinear
by COLLSP:2;
not c2,c1,c7 are_collinear
c1,
c4,
c1 are_collinear
by COLLSP:2;
hence
not
c2,
c1,
c7 are_collinear
by A11, A1, A12, HESSENBE:3;
verum end; hence
not
c2,
c7,
c1 are_collinear
by A11, A12, HESSENBE:2;
( c2,c3,c1 are_collinear & ( for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear ) ) )
not
c4 = c1
by COLLSP:2, A11;
then
c1,
c2,
c3 are_collinear
by A13, A12, HESSENBE:2;
hence
c2,
c3,
c1 are_collinear
by HESSENBE:1;
for v2, v100 being Element of (ProjectiveSpace (TOP-REAL 3)) holds
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear )hereby verum
let v2,
v100 be
Element of
(ProjectiveSpace (TOP-REAL 3));
( not v100,c7,c5 are_collinear or not c5,c7,v2 are_collinear or v100,c7,v2 are_collinear )
( not
v100,
c7,
c5 are_collinear or not
v100,
c7,
c7 are_collinear or not
c5,
c7,
v2 are_collinear or
v100,
c7,
v2 are_collinear )
by A9, HESSENBE:3;
hence
( not
v100,
c7,
c5 are_collinear or not
c5,
c7,
v2 are_collinear or
v100,
c7,
v2 are_collinear )
by COLLSP:2;
verum
end; end;
hence
contradiction
by A6, HESSENBE:3, A17, A16, A18, A19, A20, A21, A22, COLLSP:4, A15, A8, A14, A7; verum