let n be Nat; :: thesis: for Sp, Sn being Subset of () st Sp = { s where s is Point of () : ( s . n >= 0 & |.s.| = 1 ) } & Sn = { t where t is Point of () : ( t . n <= 0 & |.t.| = 1 ) } holds
( Sp is closed & Sn is closed )

let Sp, Sn be Subset of (); :: thesis: ( Sp = { s where s is Point of () : ( s . n >= 0 & |.s.| = 1 ) } & Sn = { t where t is Point of () : ( t . n <= 0 & |.t.| = 1 ) } implies ( Sp is closed & Sn is closed ) )
assume that
A1: Sp = { s where s is Point of () : ( s . n >= 0 & |.s.| = 1 ) } and
A2: Sn = { t where t is Point of () : ( t . n <= 0 & |.t.| = 1 ) } ; :: thesis: ( Sp is closed & Sn is closed )
set Tn = TOP-REAL n;
per cases ( n = 0 or n > 0 ) ;
suppose A4: n = 0 ; :: thesis: ( Sp is closed & Sn is closed )
A5: Sn = {}
proof
assume Sn <> {} ; :: thesis: contradiction
then consider x being object such that
A6: x in Sn by XBOOLE_0:def 1;
ex p being Point of () st
( x = p & p . n <= 0 & |.p.| = 1 ) by A2, A6;
hence contradiction by A4; :: thesis: verum
end;
Sp = {}
proof
assume Sp <> {} ; :: thesis: contradiction
then consider x being object such that
A7: x in Sp by XBOOLE_0:def 1;
ex p being Point of () st
( x = p & p . n >= 0 & |.p.| = 1 ) by A1, A7;
hence contradiction by A4; :: thesis: verum
end;
hence ( Sp is closed & Sn is closed ) by A5; :: thesis: verum
end;
suppose A8: n > 0 ; :: thesis: ( Sp is closed & Sn is closed )
set P2 = { p where p is Point of () : 0 < p /. n } ;
set P1 = { p where p is Point of () : 0 > p /. n } ;
A9: { p where p is Point of () : 0 > p /. n } c= the carrier of ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of () : 0 > p /. n } or x in the carrier of () )
assume x in { p where p is Point of () : 0 > p /. n } ; :: thesis: x in the carrier of ()
then ex p being Point of () st
( p = x & 0 > p /. n ) ;
hence x in the carrier of () ; :: thesis: verum
end;
{ p where p is Point of () : 0 < p /. n } c= the carrier of ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of () : 0 < p /. n } or x in the carrier of () )
assume x in { p where p is Point of () : 0 < p /. n } ; :: thesis: x in the carrier of ()
then ex p being Point of () st
( p = x & 0 < p /. n ) ;
hence x in the carrier of () ; :: thesis: verum
end;
then reconsider P1 = { p where p is Point of () : 0 > p /. n } , P2 = { p where p is Point of () : 0 < p /. n } as Subset of () by A9;
n in Seg n by ;
then reconsider P1 = P1, P2 = P2 as open Subset of () by ;
set S2 = (P2 `) /\ (Sphere ((0. ()),1));
A10: Sn c= (P2 `) /\ (Sphere ((0. ()),1))
proof
let xx be object ; :: according to TARSKI:def 3 :: thesis: ( not xx in Sn or xx in (P2 `) /\ (Sphere ((0. ()),1)) )
assume xx in Sn ; :: thesis: xx in (P2 `) /\ (Sphere ((0. ()),1))
then consider p being Point of () such that
A11: xx = p and
A12: p . n <= 0 and
A13: |.p.| = 1 by A2;
p - (0. ()) = p by RLVECT_1:13;
then A14: p in Sphere ((0. ()),1) by A13;
len p = n by CARD_1:def 7;
then A15: dom p = Seg n by FINSEQ_1:def 3;
A16: not p in P2
proof
assume p in P2 ; :: thesis: contradiction
then ex q being Point of () st
( p = q & 0 < q /. n ) ;
hence contradiction by A15, PARTFUN1:def 6, FINSEQ_1:3, A8, A12; :: thesis: verum
end;
P2 ` = ([#] ()) \ P2 by SUBSET_1:def 4;
then p in P2 ` by ;
hence xx in (P2 `) /\ (Sphere ((0. ()),1)) by ; :: thesis: verum
end;
A17: (P2 `) /\ (Sphere ((0. ()),1)) c= Sn
proof
let xx be object ; :: according to TARSKI:def 3 :: thesis: ( not xx in (P2 `) /\ (Sphere ((0. ()),1)) or xx in Sn )
A18: P2 ` = ([#] ()) \ P2 by SUBSET_1:def 4;
assume A19: xx in (P2 `) /\ (Sphere ((0. ()),1)) ; :: thesis: xx in Sn
then reconsider p = xx as Point of () ;
len p = n by CARD_1:def 7;
then dom p = Seg n by FINSEQ_1:def 3;
then A20: p /. n = p . n by ;
A21: p in P2 ` by ;
A22: p . n <= 0
proof
assume p . n > 0 ; :: thesis: contradiction
then p in P2 by A20;
hence contradiction by A21, A18, XBOOLE_0:def 5; :: thesis: verum
end;
p in Sphere ((0. ()),1) by ;
then |.p.| = 1 by TOPREAL9:12;
hence xx in Sn by ; :: thesis: verum
end;
set S1 = (P1 `) /\ (Sphere ((0. ()),1));
A23: (P1 `) /\ (Sphere ((0. ()),1)) c= Sp
proof
let xx be object ; :: according to TARSKI:def 3 :: thesis: ( not xx in (P1 `) /\ (Sphere ((0. ()),1)) or xx in Sp )
A24: P1 ` = ([#] ()) \ P1 by SUBSET_1:def 4;
assume A25: xx in (P1 `) /\ (Sphere ((0. ()),1)) ; :: thesis: xx in Sp
then reconsider p = xx as Point of () ;
len p = n by CARD_1:def 7;
then dom p = Seg n by FINSEQ_1:def 3;
then A26: p /. n = p . n by ;
A27: p in P1 ` by ;
A28: p . n >= 0
proof
assume p . n < 0 ; :: thesis: contradiction
then p in P1 by A26;
hence contradiction by A27, A24, XBOOLE_0:def 5; :: thesis: verum
end;
p in Sphere ((0. ()),1) by ;
then |.p.| = 1 by TOPREAL9:12;
hence xx in Sp by ; :: thesis: verum
end;
Sp c= (P1 `) /\ (Sphere ((0. ()),1))
proof
let xx be object ; :: according to TARSKI:def 3 :: thesis: ( not xx in Sp or xx in (P1 `) /\ (Sphere ((0. ()),1)) )
assume xx in Sp ; :: thesis: xx in (P1 `) /\ (Sphere ((0. ()),1))
then consider p being Point of () such that
A29: xx = p and
A30: p . n >= 0 and
A31: |.p.| = 1 by A1;
p - (0. ()) = p by RLVECT_1:13;
then A32: p in Sphere ((0. ()),1) by A31;
len p = n by CARD_1:def 7;
then A33: dom p = Seg n by FINSEQ_1:def 3;
A34: not p in P1
proof
assume p in P1 ; :: thesis: contradiction
then ex q being Point of () st
( p = q & 0 > q /. n ) ;
hence contradiction by A33, PARTFUN1:def 6, FINSEQ_1:3, A8, A30; :: thesis: verum
end;
P1 ` = ([#] ()) \ P1 by SUBSET_1:def 4;
then p in P1 ` by ;
hence xx in (P1 `) /\ (Sphere ((0. ()),1)) by ; :: thesis: verum
end;
hence ( Sp is closed & Sn is closed ) by ; :: thesis: verum
end;
end;