let n31, n32, n33 be Element of F_Real; 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); ( 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
; 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)
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;
now ( |(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;
|(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;
verum end;
hence
0 < (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) * (((n31 * (v . 1)) + (n32 * (v . 2))) + n33)
by A7, A6, Th28; verum