let o, p1, p2, p3, q1, q2, q3, r1, r2, r3 be Element of (ProjectiveSpace (TOP-REAL 3)); ( o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear implies r1,r2,r3 are_collinear )
assume that
A1:
o <> p2
and
A2:
o <> p3
and
A3:
p2 <> p3
and
A4:
p1 <> p2
and
A5:
p1 <> p3
and
A6:
o <> q2
and
A7:
o <> q3
and
A8:
q2 <> q3
and
A9:
q1 <> q2
and
A10:
q1 <> q3
and
A11:
not o,p1,q1 are_collinear
and
A12:
o,p1,p2 are_collinear
and
A13:
o,p1,p3 are_collinear
and
A14:
o,q1,q2 are_collinear
and
A15:
o,q1,q3 are_collinear
and
A16:
p1,q2,r3 are_collinear
and
A17:
q1,p2,r3 are_collinear
and
A18:
p1,q3,r2 are_collinear
and
A19:
p3,q1,r2 are_collinear
and
A20:
p2,q3,r1 are_collinear
and
A21:
p3,q2,r1 are_collinear
; r1,r2,r3 are_collinear
p1,p2,p3 are_collinear
by A11, A12, A13, Th12;
then consider u1, u2, u3 being Element of (TOP-REAL 3) such that
A22:
p1 = Dir u1
and
A23:
p2 = Dir u2
and
A24:
p3 = Dir u3
and
A25:
not u1 is zero
and
A26:
not u2 is zero
and
A27:
not u3 is zero
and
A28:
u1,u2,u3 are_LinDep
by ANPROJ_2:23;
A29:
|{u1,u2,u3}| = 0
by A28, ANPROJ_8:43;
then A30:
|(u1,(u2 <X> u3))| = 0
by EUCLID_5:def 5;
set x1 = ((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2));
set x2 = ((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3));
set x3 = ((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1));
A31:
u1 = |[(u1 `1),(u1 `2),(u1 `3)]|
by EUCLID_5:3;
A32:
u2 <X> u3 = |[(((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))),(((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))),(((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1)))]|
by EUCLID_5:def 4;
A33: 0 =
|(u1,(u2 <X> u3))|
by A29, EUCLID_5:def 5
.=
(((u1 `1) * (((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2)))) + ((u1 `2) * (((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))))) + ((u1 `3) * (((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))))
by A31, A32, EUCLID_5:30
;
A34: (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (u1 . 1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (u1 . 2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (u1 . 3)) =
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (u1 . 1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (u1 . 2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (u1 `3))
by EUCLID_5:def 3
.=
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (u1 . 1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (u1 `2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (u1 `3))
by EUCLID_5:def 2
.=
0
by A33, EUCLID_5:def 1
;
A35: (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (u2 . 1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (u2 . 2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (u2 . 3)) =
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (u2 . 1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (u2 . 2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (u2 `3))
by EUCLID_5:def 3
.=
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (u2 . 1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (u2 `2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (u2 `3))
by EUCLID_5:def 2
.=
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (u2 `1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (u2 `2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (u2 `3))
by EUCLID_5:def 1
.=
0
;
A36: (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (u3 . 1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (u3 . 2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (u3 . 3)) =
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (u3 . 1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (u3 . 2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (u3 `3))
by EUCLID_5:def 3
.=
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (u3 . 1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (u3 `2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (u3 `3))
by EUCLID_5:def 2
.=
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (u3 `1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (u3 `2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (u3 `3))
by EUCLID_5:def 1
.=
0
;
q1,q2,q3 are_collinear
by A11, A14, A15, Th13;
then consider v1, v2, v3 being Element of (TOP-REAL 3) such that
A37:
q1 = Dir v1
and
A38:
q2 = Dir v2
and
A39:
q3 = Dir v3
and
A40:
not v1 is zero
and
A41:
not v2 is zero
and
A42:
not v3 is zero
and
A43:
v1,v2,v3 are_LinDep
by ANPROJ_2:23;
A44:
|{v1,v2,v3}| = 0
by A43, ANPROJ_8:43;
then A45:
|(v1,(v2 <X> v3))| = 0
by EUCLID_5:def 5;
set y1 = ((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2));
set y2 = ((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3));
set y3 = ((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1));
A46:
v1 = |[(v1 `1),(v1 `2),(v1 `3)]|
by EUCLID_5:3;
A47:
v2 <X> v3 = |[(((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))),(((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))),(((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))]|
by EUCLID_5:def 4;
A48: 0 =
|(v1,(v2 <X> v3))|
by A44, EUCLID_5:def 5
.=
(((v1 `1) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))) + ((v1 `2) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))) + ((v1 `3) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))))
by A46, A47, EUCLID_5:30
;
A49: (((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (v1 . 1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (v1 . 2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (v1 . 3)) =
(((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (v1 . 1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (v1 . 2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (v1 `3))
by EUCLID_5:def 3
.=
(((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (v1 . 1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (v1 `2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (v1 `3))
by EUCLID_5:def 2
.=
0
by A48, EUCLID_5:def 1
;
A50: (((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (v2 . 1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (v2 . 2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (v2 . 3)) =
(((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (v2 . 1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (v2 . 2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (v2 `3))
by EUCLID_5:def 3
.=
(((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (v2 . 1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (v2 `2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (v2 `3))
by EUCLID_5:def 2
.=
(((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (v2 `1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (v2 `2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (v2 `3))
by EUCLID_5:def 1
.=
0
;
A51: (((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (v3 . 1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (v3 . 2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (v3 . 3)) =
(((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (v3 . 1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (v3 . 2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (v3 `3))
by EUCLID_5:def 3
.=
(((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (v3 . 1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (v3 `2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (v3 `3))
by EUCLID_5:def 2
.=
(((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (v3 `1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (v3 `2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (v3 `3))
by EUCLID_5:def 1
.=
0
;
set xa = (((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)));
set xb = (((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)));
set xc = (((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)));
set xd = ((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))));
set xe = ((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))));
set xf = ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))));
A52:
for u being Point of (TOP-REAL 3) holds qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),u) = |(u,(u2 <X> u3))| * |(u,(v2 <X> v3))|
proof
let u be
Point of
(TOP-REAL 3);
qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),u) = |(u,(u2 <X> u3))| * |(u,(v2 <X> v3))|
A53:
(
u . 1
= u `1 &
u . 2
= u `2 &
u . 3
= u `3 )
by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
now ( qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),u) = ((((((((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))) * (u `1)) * (u `1)) + ((((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) * (u `2)) * (u `2))) + ((((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) * (u `3)) * (u `3))) + (((((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))) * (u `1)) * (u `2))) + (((((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))) * (u `1)) * (u `3))) + (((((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))) * (u `2)) * (u `3)) & |(u,(u2 <X> u3))| = (((u `1) * (((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2)))) + ((u `2) * (((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))))) + ((u `3) * (((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1)))) & |(u,(v2 <X> v3))| = (((u `1) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))) + ((u `2) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))) + ((u `3) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) )thus
qfconic (
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),
((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),
((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),
u)
= ((((((((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))) * (u `1)) * (u `1)) + ((((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) * (u `2)) * (u `2))) + ((((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) * (u `3)) * (u `3))) + (((((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))) * (u `1)) * (u `2))) + (((((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))) * (u `1)) * (u `3))) + (((((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))) * (u `2)) * (u `3))
by A53;
( |(u,(u2 <X> u3))| = (((u `1) * (((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2)))) + ((u `2) * (((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))))) + ((u `3) * (((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1)))) & |(u,(v2 <X> v3))| = (((u `1) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))) + ((u `2) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))) + ((u `3) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) )thus |(u,(u2 <X> u3))| =
|(|[(u `1),(u `2),(u `3)]|,|[(((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))),(((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))),(((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1)))]|)|
by EUCLID_5:27, A32
.=
(((u `1) * (((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2)))) + ((u `2) * (((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))))) + ((u `3) * (((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))))
by EUCLID_5:30
;
|(u,(v2 <X> v3))| = (((u `1) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))) + ((u `2) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))) + ((u `3) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))))thus |(u,(v2 <X> v3))| =
|(|[(u `1),(u `2),(u `3)]|,|[(((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))),(((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))),(((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))]|)|
by EUCLID_5:27, A47
.=
(((u `1) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))) + ((u `2) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))) + ((u `3) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))))
by EUCLID_5:30
;
verum end;
hence
qfconic (
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),
((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),
((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),
u)
= |(u,(u2 <X> u3))| * |(u,(v2 <X> v3))|
;
verum
end;
A54:
now ( qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),u1) = 0 & qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),u2) = 0 & qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),u3) = 0 & qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),v1) = 0 & qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),v2) = 0 & qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),v3) = 0 )thus qfconic (
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),
((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),
((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),
u1) =
((((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (u1 . 1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (u1 . 2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (u1 . 3))) * ((((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (u1 . 1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (u1 . 2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (u1 . 3)))
.=
0
by A34
;
( qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),u2) = 0 & qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),u3) = 0 & qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),v1) = 0 & qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),v2) = 0 & qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),v3) = 0 )thus qfconic (
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),
((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),
((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),
u2) =
((((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (u2 . 1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (u2 . 2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (u2 . 3))) * ((((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (u2 . 1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (u2 . 2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (u2 . 3)))
.=
0
by A35
;
( qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),u3) = 0 & qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),v1) = 0 & qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),v2) = 0 & qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),v3) = 0 )thus qfconic (
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),
((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),
((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),
u3) =
((((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (u3 . 1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (u3 . 2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (u3 . 3))) * ((((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (u3 . 1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (u3 . 2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (u3 . 3)))
.=
0
by A36
;
( qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),v1) = 0 & qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),v2) = 0 & qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),v3) = 0 )thus qfconic (
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),
((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),
((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),
v1) =
((((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (v1 . 1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (v1 . 2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (v1 . 3))) * ((((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (v1 . 1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (v1 . 2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (v1 . 3)))
.=
0
by A49
;
( qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),v2) = 0 & qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),v3) = 0 )thus qfconic (
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),
((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),
((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),
v2) =
((((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (v2 . 1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (v2 . 2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (v2 . 3))) * ((((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (v2 . 1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (v2 . 2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (v2 . 3)))
.=
0
by A50
;
qfconic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),v3) = 0 thus qfconic (
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),
((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),
((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))),
v3) =
((((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (v3 . 1)) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (v3 . 2))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (v3 . 3))) * ((((((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) * (v3 . 1)) + ((((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) * (v3 . 2))) + ((((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) * (v3 . 3)))
.=
0
by A51
;
verum end;
now ( p1,p2,p3,q1,q2,q3,r1,r2,r3 are_in_Pascal_configuration & ( (((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) <> 0 or (((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) <> 0 or (((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) <> 0 or ((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))) <> 0 or ((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))) <> 0 or ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) <> 0 ) & {p1,p2,p3,q1,q2,q3} c= conic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))))) )thus
p1,
p2,
p3,
q1,
q2,
q3,
r1,
r2,
r3 are_in_Pascal_configuration
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, Th19;
( ( (((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) <> 0 or (((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) <> 0 or (((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) <> 0 or ((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))) <> 0 or ((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))) <> 0 or ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) <> 0 ) & {p1,p2,p3,q1,q2,q3} c= conic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))))) )thus
(
(((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) <> 0 or
(((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) <> 0 or
(((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) <> 0 or
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))) <> 0 or
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))) <> 0 or
((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) <> 0 )
{p1,p2,p3,q1,q2,q3} c= conic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))))proof
assume
(
(((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))) = 0 &
(((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))) = 0 &
(((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))) = 0 &
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))) = 0 &
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))) = 0 &
((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) = 0 )
;
contradiction
then reconsider xa =
(((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))),
xb =
(((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))),
xc =
(((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1))),
xd =
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),
xe =
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),
xf =
((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) as
zero Real by ORDINAL1:def 14;
set w =
(1 / 2) * (u1 + v1);
A55:
(1 / 2) * (u1 + v1) = ((1 / 2) * u1) + ((1 / 2) * v1)
by RVSUM_1:51;
0 =
qfconic (
xa,
xb,
xc,
xd,
xe,
xf,
((1 / 2) * (u1 + v1)))
.=
|((((1 / 2) * u1) + ((1 / 2) * v1)),(u2 <X> u3))| * |((((1 / 2) * u1) + ((1 / 2) * v1)),(v2 <X> v3))|
by A55, A52
.=
(|(((1 / 2) * u1),(u2 <X> u3))| + |(((1 / 2) * v1),(u2 <X> u3))|) * |((((1 / 2) * u1) + ((1 / 2) * v1)),(v2 <X> v3))|
by EUCLID_2:18
.=
(((1 / 2) * |(u1,(u2 <X> u3))|) + |(((1 / 2) * v1),(u2 <X> u3))|) * |((((1 / 2) * u1) + ((1 / 2) * v1)),(v2 <X> v3))|
by EUCLID_2:19
.=
|(((1 / 2) * v1),(u2 <X> u3))| * (|(((1 / 2) * u1),(v2 <X> v3))| + |(((1 / 2) * v1),(v2 <X> v3))|)
by A30, EUCLID_2:18
.=
|(((1 / 2) * v1),(u2 <X> u3))| * (|(((1 / 2) * u1),(v2 <X> v3))| + ((1 / 2) * |(v1,(v2 <X> v3))|))
by EUCLID_2:19
.=
((1 / 2) * |(v1,(u2 <X> u3))|) * |(((1 / 2) * u1),(v2 <X> v3))|
by A45, EUCLID_2:19
.=
((1 / 2) * |(v1,(u2 <X> u3))|) * ((1 / 2) * |(u1,(v2 <X> v3))|)
by EUCLID_2:19
.=
((1 / 4) * |(v1,(u2 <X> u3))|) * |(u1,(v2 <X> v3))|
;
then
|(v1,(u2 <X> u3))| * |(u1,(v2 <X> v3))| = 0
;
then
|{v1,u2,u3}| * |(u1,(v2 <X> v3))| = 0
by EUCLID_5:def 5;
then
|{v1,u2,u3}| * |{u1,v2,v3}| = 0
by EUCLID_5:def 5;
then
(
|{v1,u2,u3}| = 0 or
|{u1,v2,v3}| = 0 )
by XCMPLX_1:6;
then A56:
(
q1,
p2,
p3 are_collinear or
p1,
q2,
q3 are_collinear )
by A22, A23, A24, A25, A26, A27, A37, A38, A39, A40, A41, A42, BKMODEL1:1;
p1,
p2,
p3,
q1,
q2,
q3,
r1,
r2,
r3 are_in_Pascal_configuration
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, Th19;
hence
contradiction
by A56, COLLSP:8;
verum
end; thus
{p1,p2,p3,q1,q2,q3} c= conic (
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),
((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),
((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))))
verumproof
now for o being object st o in {p1,p2,p3,q1,q2,q3} holds
o in conic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))))let o be
object ;
( o in {p1,p2,p3,q1,q2,q3} implies o in conic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))))) )assume
o in {p1,p2,p3,q1,q2,q3}
;
o in conic (((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))))then
(
o = p1 or
o = p2 or
o = p3 or
o = q1 or
o = q2 or
o = q3 )
by ENUMSET1:def 4;
hence
o in conic (
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),
((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),
((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))))
by A54, A22, A23, A24, A25, A26, A27, A37, A38, A39, A40, A41, A42, PASCAL:11;
verum end;
hence
{p1,p2,p3,q1,q2,q3} c= conic (
((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2)))),
((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))),
((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3)))) + ((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `2) * (u3 `3)) - ((u2 `3) * (u3 `2))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `2) * (v3 `3)) - ((v2 `3) * (v3 `2))))),
(((((u2 `3) * (u3 `1)) - ((u2 `1) * (u3 `3))) * (((v2 `1) * (v3 `2)) - ((v2 `2) * (v3 `1)))) + ((((u2 `1) * (u3 `2)) - ((u2 `2) * (u3 `1))) * (((v2 `3) * (v3 `1)) - ((v2 `1) * (v3 `3))))))
by TARSKI:def 3;
verum
end; end;
hence
r1,r2,r3 are_collinear
by PASCAL:36; verum