let n be Nat; :: thesis: for Sp, Sn being Subset of (TOP-REAL n) st Sp = { s where s is Point of (TOP-REAL n) : ( s . n >= 0 & |.s.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL n) : ( t . n <= 0 & |.t.| = 1 ) } holds
( Sp is closed & Sn is closed )
let Sp, Sn be Subset of (TOP-REAL n); :: thesis: ( Sp = { s where s is Point of (TOP-REAL n) : ( s . n >= 0 & |.s.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL n) : ( t . n <= 0 & |.t.| = 1 ) } implies ( Sp is closed & Sn is closed ) )
assume that
A1: Sp = { s where s is Point of (TOP-REAL n) : ( s . n >= 0 & |.s.| = 1 ) } and
A2: Sn = { t where t is Point of (TOP-REAL n) : ( 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 (TOP-REAL n) 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 (TOP-REAL n) 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 (TOP-REAL n) : 0 < p /. n } ;
set P1 = { p where p is Point of (TOP-REAL n) : 0 > p /. n } ;
A9: { p where p is Point of (TOP-REAL n) : 0 > p /. n } c= the carrier of (TOP-REAL n)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL n) : 0 > p /. n } or x in the carrier of (TOP-REAL n) )
assume x in { p where p is Point of (TOP-REAL n) : 0 > p /. n } ; :: thesis: x in the carrier of (TOP-REAL n)
then ex p being Point of (TOP-REAL n) st
( p = x & 0 > p /. n ) ;
hence x in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

{ p where p is Point of (TOP-REAL n) : 0 < p /. n } c= the carrier of (TOP-REAL n)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL n) : 0 < p /. n } or x in the carrier of (TOP-REAL n) )
assume x in { p where p is Point of (TOP-REAL n) : 0 < p /. n } ; :: thesis: x in the carrier of (TOP-REAL n)
then ex p being Point of (TOP-REAL n) st
( p = x & 0 < p /. n ) ;
hence x in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

then reconsider P1 = { p where p is Point of (TOP-REAL n) : 0 > p /. n } , P2 = { p where p is Point of (TOP-REAL n) : 0 < p /. n } as Subset of (TOP-REAL n) by A9;
n in Seg n by FINSEQ_1:3, A8;
then reconsider P1 = P1, P2 = P2 as open Subset of (TOP-REAL n) by JORDAN2B:13, JORDAN2B:12;
set S2 = (P2 `) /\ (Sphere ((0. (TOP-REAL n)),1));
A10: Sn c= (P2 `) /\ (Sphere ((0. (TOP-REAL n)),1))

proof

let xx be object ; :: according to TARSKI:def 3 :: thesis: ( not xx in Sn or xx in (P2 `) /\ (Sphere ((0. (TOP-REAL n)),1)) )
assume xx in Sn ; :: thesis: xx in (P2 `) /\ (Sphere ((0. (TOP-REAL n)),1))
then consider p being Point of (TOP-REAL n) such that
A11: xx = p and
A12: p . n <= 0 and
A13: |.p.| = 1 by A2;
p - (0. (TOP-REAL n)) = p by RLVECT_1:13;
then A14: p in Sphere ((0. (TOP-REAL n)),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 (TOP-REAL n) st
( p = q & 0 < q /. n ) ;
hence contradiction by A15, PARTFUN1:def 6, FINSEQ_1:3, A8, A12; :: thesis: verum

end;

P2 ` = ([#] (TOP-REAL n)) \ P2 by SUBSET_1:def 4;
then p in P2 ` by A16, XBOOLE_0:def 5;
hence xx in (P2 `) /\ (Sphere ((0. (TOP-REAL n)),1)) by A14, XBOOLE_0:def 4, A11; :: thesis: verum

end;

A17: (P2 `) /\ (Sphere ((0. (TOP-REAL n)),1)) c= Sn

proof

let xx be object ; :: according to TARSKI:def 3 :: thesis: ( not xx in (P2 `) /\ (Sphere ((0. (TOP-REAL n)),1)) or xx in Sn )
A18: P2 ` = ([#] (TOP-REAL n)) \ P2 by SUBSET_1:def 4;
assume A19: xx in (P2 `) /\ (Sphere ((0. (TOP-REAL n)),1)) ; :: thesis: xx in Sn
then reconsider p = xx as Point of (TOP-REAL n) ;
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 PARTFUN1:def 6, FINSEQ_1:3, A8;
A21: p in P2 ` by A19, XBOOLE_0:def 4;
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. (TOP-REAL n)),1) by A19, XBOOLE_0:def 4;
then |.p.| = 1 by TOPREAL9:12;
hence xx in Sn by A22, A2; :: thesis: verum

end;

set S1 = (P1 `) /\ (Sphere ((0. (TOP-REAL n)),1));
A23: (P1 `) /\ (Sphere ((0. (TOP-REAL n)),1)) c= Sp

proof

let xx be object ; :: according to TARSKI:def 3 :: thesis: ( not xx in (P1 `) /\ (Sphere ((0. (TOP-REAL n)),1)) or xx in Sp )
A24: P1 ` = ([#] (TOP-REAL n)) \ P1 by SUBSET_1:def 4;
assume A25: xx in (P1 `) /\ (Sphere ((0. (TOP-REAL n)),1)) ; :: thesis: xx in Sp
then reconsider p = xx as Point of (TOP-REAL n) ;
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 PARTFUN1:def 6, FINSEQ_1:3, A8;
A27: p in P1 ` by A25, XBOOLE_0:def 4;
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. (TOP-REAL n)),1) by A25, XBOOLE_0:def 4;
then |.p.| = 1 by TOPREAL9:12;
hence xx in Sp by A28, A1; :: thesis: verum

end;

Sp c= (P1 `) /\ (Sphere ((0. (TOP-REAL n)),1))

proof

let xx be object ; :: according to TARSKI:def 3 :: thesis: ( not xx in Sp or xx in (P1 `) /\ (Sphere ((0. (TOP-REAL n)),1)) )
assume xx in Sp ; :: thesis: xx in (P1 `) /\ (Sphere ((0. (TOP-REAL n)),1))
then consider p being Point of (TOP-REAL n) such that
A29: xx = p and
A30: p . n >= 0 and
A31: |.p.| = 1 by A1;
p - (0. (TOP-REAL n)) = p by RLVECT_1:13;
then A32: p in Sphere ((0. (TOP-REAL n)),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 (TOP-REAL n) st
( p = q & 0 > q /. n ) ;
hence contradiction by A33, PARTFUN1:def 6, FINSEQ_1:3, A8, A30; :: thesis: verum

end;

P1 ` = ([#] (TOP-REAL n)) \ P1 by SUBSET_1:def 4;
then p in P1 ` by A34, XBOOLE_0:def 5;
hence xx in (P1 `) /\ (Sphere ((0. (TOP-REAL n)),1)) by A32, XBOOLE_0:def 4, A29; :: thesis: verum

end;

hence ( Sp is closed & Sn is closed ) by A10, A17, XBOOLE_0:def 10, A23; :: thesis: verum

end;

end;