Dir101 in conic (1,1,(- 1),0,0,0)

proof

Dir101 in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0 }

proof

now :: thesis: for u being Element of (TOP-REAL 3) st not u is zero & Dir101 = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0

let u be Element of (TOP-REAL 3); :: thesis: ( not u is zero & Dir101 = Dir u implies qfconic (1,1,(- 1),0,0,0,u) = 0 )
assume A1: ( not u is zero & Dir101 = Dir u ) ; :: thesis: qfconic (1,1,(- 1),0,0,0,u) = 0
not |[1,0,1]| is zero by EUCLID_5:4, FINSEQ_1:78;
then are_Prop u,|[1,0,1]| by A1, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A2: u = a * |[1,0,1]| by ANPROJ_1:1;
u = |[(a * 1),(a * 0),(a * 1)]| by A2, EUCLID_5:8
.= |[a,0,a]| ;
then ( u `1 = a & u `2 = 0 & u `3 = a ) by EUCLID_5:2;
then A3: ( u . 1 = a & u . 2 = 0 & u . 3 = a ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
thus qfconic (1,1,(- 1),0,0,0,u) = ((((((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 PASCAL:def 1
.= 0 by A3 ; :: thesis: verum

end;

hence Dir101 in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (1,1,(- 1),0,0,0,u) = 0 } ; :: thesis: verum

end;

hence Dir101 in conic (1,1,(- 1),0,0,0) by PASCAL:def 2; :: thesis: verum

end;

hence conic (1,1,(- 1),0,0,0) is non empty Subset of (ProjectiveSpace (TOP-REAL 3)) ; :: thesis: verum