let n31, n32, n33 be Element of F_Real; :: thesis: for u, v being Element of (TOP-REAL 2) st u in inside_of_circle (0,0,1) & v in circle (0,0,1) & ( for w being Element of (TOP-REAL 2) st w in closed_inside_of_circle (0,0,1) holds
((n31 * (w . 1)) + (n32 * (w . 2))) + n33 <> 0 ) holds
0 < (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) * (((n31 * (v . 1)) + (n32 * (v . 2))) + n33)
let u, v be Element of (TOP-REAL 2); :: thesis: ( u in inside_of_circle (0,0,1) & v in circle (0,0,1) & ( for w being Element of (TOP-REAL 2) st w in closed_inside_of_circle (0,0,1) holds
((n31 * (w . 1)) + (n32 * (w . 2))) + n33 <> 0 ) implies 0 < (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) * (((n31 * (v . 1)) + (n32 * (v . 2))) + n33) )
assume that
A1: u in inside_of_circle (0,0,1) and
A2: v in circle (0,0,1) and
A3: for w being Element of (TOP-REAL 2) st w in closed_inside_of_circle (0,0,1) holds
((n31 * (w . 1)) + (n32 * (w . 2))) + n33 <> 0 ; :: thesis: 0 < (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) * (((n31 * (v . 1)) + (n32 * (v . 2))) + n33)
set B = closed_inside_of_circle (0,0,1);
set A = { x where x is Element of (TOP-REAL 3) : ( |[(x `1),(x `2)]| in closed_inside_of_circle (0,0,1) & x `3 = 1 ) } ;
{ x where x is Element of (TOP-REAL 3) : ( |[(x `1),(x `2)]| in closed_inside_of_circle (0,0,1) & x `3 = 1 ) } c= the carrier of (TOP-REAL 3)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of (TOP-REAL 3) : ( |[(x `1),(x `2)]| in closed_inside_of_circle (0,0,1) & x `3 = 1 ) } or x in the carrier of (TOP-REAL 3) )
assume x in { x where x is Element of (TOP-REAL 3) : ( |[(x `1),(x `2)]| in closed_inside_of_circle (0,0,1) & x `3 = 1 ) } ; :: thesis: x in the carrier of (TOP-REAL 3)
then ex y being Element of (TOP-REAL 3) st
( x = y & |[(y `1),(y `2)]| in closed_inside_of_circle (0,0,1) & y `3 = 1 ) ;
hence x in the carrier of (TOP-REAL 3) ; :: thesis: verum
end;
then reconsider A = { x where x is Element of (TOP-REAL 3) : ( |[(x `1),(x `2)]| in closed_inside_of_circle (0,0,1) & x `3 = 1 ) } as Subset of (TOP-REAL 3) ;
reconsider A = A as non empty convex Subset of (TOP-REAL 3) by Th26;
reconsider n = |[n31,n32,n33]|, u9 = |[(u . 1),(u . 2),1]|, v9 = |[(v . 1),(v . 2),1]| as Element of (TOP-REAL 3) ;
( inside_of_circle (0,0,1) c= closed_inside_of_circle (0,0,1) & circle (0,0,1) c= closed_inside_of_circle (0,0,1) ) by TOPREAL9:46, TOPREAL9:53;
then ( u in closed_inside_of_circle (0,0,1) & v in closed_inside_of_circle (0,0,1) ) by A1, A2;
then A4: ( |[(u `1),(u `2)]| in closed_inside_of_circle (0,0,1) & |[(v `1),(v `2)]| in closed_inside_of_circle (0,0,1) ) by EUCLID:53;
A5: ( u9 `1 = u . 1 & u9 `2 = u . 2 & u9 `3 = 1 & v9 `1 = v . 1 & v9 `2 = v . 2 & v9 `3 = 1 ) by EUCLID_5:2;
A6: ( u9 in A & v9 in A ) by A5, A4;
A7: now :: thesis: for w being Element of (TOP-REAL 3) st w in A holds
|(n,w)| <> 0
let w be Element of (TOP-REAL 3); :: thesis: ( w in A implies |(n,w)| <> 0 )
assume w in A ; :: thesis: |(n,w)| <> 0
then consider x being Element of (TOP-REAL 3) such that
A8: w = x and
A9: |[(x `1),(x `2)]| in closed_inside_of_circle (0,0,1) and
A10: x `3 = 1 ;
reconsider v = |[(x `1),(x `2)]| as Element of (TOP-REAL 2) ;
now :: thesis: ( |(n,w)| = ((n31 * (w . 1)) + (n32 * (w . 2))) + n33 & w . 1 = v . 1 & w . 2 = v . 2 )
w . 3 = 1 by A8, A10, EUCLID_5:def 3;
hence |(n,w)| = ((n31 * (w . 1)) + (n32 * (w . 2))) + n33 by Th27; :: thesis: ( w . 1 = v . 1 & w . 2 = v . 2 )
thus w . 1 = w `1 by EUCLID_5:def 1
.= v `1 by A8, EUCLID:52
.= v . 1 ; :: thesis: w . 2 = v . 2
thus w . 2 = w `2 by EUCLID_5:def 2
.= v `2 by A8, EUCLID:52
.= v . 2 ; :: thesis: verum
end;
hence |(n,w)| <> 0 by A3, A9; :: thesis: verum
end;
now :: thesis: ( |(n,u9)| = ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 & |(n,v9)| = ((n31 * (v . 1)) + (n32 * (v . 2))) + n33 )
( n = <*n31,n32,n33*> & u9 . 3 = 1 ) by A5, EUCLID_5:def 3;
then |(n,u9)| = ((n31 * (u9 . 1)) + (n32 * (u9 . 2))) + n33 by Th27;
then |(n,u9)| = ((n31 * (u9 `1)) + (n32 * (u9 . 2))) + n33 by EUCLID_5:def 1;
hence |(n,u9)| = ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 by A5, EUCLID_5:def 2; :: thesis: |(n,v9)| = ((n31 * (v . 1)) + (n32 * (v . 2))) + n33
( n = <*n31,n32,n33*> & v9 . 3 = 1 ) by A5, EUCLID_5:def 3;
then |(n,v9)| = ((n31 * (v9 . 1)) + (n32 * (v9 . 2))) + n33 by Th27;
then |(n,v9)| = ((n31 * (v9 `1)) + (n32 * (v9 . 2))) + n33 by EUCLID_5:def 1;
hence |(n,v9)| = ((n31 * (v . 1)) + (n32 * (v . 2))) + n33 by A5, EUCLID_5:def 2; :: thesis: verum
end;
hence 0 < (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) * (((n31 * (v . 1)) + (n32 * (v . 2))) + n33) by A7, A6, Th28; :: thesis: verum