let u be Element of (TOP-REAL 3); :: thesis: ( qfconic (1,1,(- 1),0,0,0,u) = 0 & u . 3 = 1 implies |[(u . 1),(u . 2)]| in Sphere ((0. (TOP-REAL 2)),1) )
assume that
A1: qfconic (1,1,(- 1),0,0,0,u) = 0 and
A2: u . 3 = 1 ; :: thesis: |[(u . 1),(u . 2)]| in Sphere ((0. (TOP-REAL 2)),1)
0 = ((((((1 * (u . 1)) * (u . 1)) + ((1 * (u . 2)) * (u . 2))) + (((- 1) * (u . 3)) * (u . 3))) + ((0 * (u . 1)) * (u . 2))) + ((0 * (u . 1)) * (u . 3))) + ((0 * (u . 2)) * (u . 3)) by A1, PASCAL:def 1
.= (((u . 1) ^2) + ((u . 2) ^2)) - 1 by A2 ;
then |[(u . 1),(u . 2)]| in circle (0,0,1) by Th11;
hence |[(u . 1),(u . 2)]| in Sphere ((0. (TOP-REAL 2)),1) by EUCLID:54, TOPREAL9:52; :: thesis: verum