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;

( 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 )
;

end;

suppose A4:
n = 0
; :: thesis: ( Sp is closed & Sn is closed )

A5:
Sn = {}

end;proof

Sp = {}
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;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

proof

hence
( Sp is closed & Sn is closed )
by A5; :: thesis: verum
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;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

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)

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))

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

end;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

{ p where p is Point of (TOP-REAL n) : 0 < p /. n } c= the carrier of (TOP-REAL n)
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;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

proof

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;
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;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

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

A17:
(P2 `) /\ (Sphere ((0. (TOP-REAL n)),1)) c= Sn
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

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;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

P2 ` = ([#] (TOP-REAL n)) \ P2
by SUBSET_1:def 4;
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;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

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

proof

set S1 = (P1 `) /\ (Sphere ((0. (TOP-REAL n)),1));
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

then |.p.| = 1 by TOPREAL9:12;

hence xx in Sn by A22, A2; :: thesis: verum

end;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

p in Sphere ((0. (TOP-REAL n)),1)
by A19, XBOOLE_0:def 4;
assume
p . n > 0
; :: thesis: contradiction

then p in P2 by A20;

hence contradiction by A21, A18, XBOOLE_0:def 5; :: thesis: verum

end;then p in P2 by A20;

hence contradiction by A21, A18, XBOOLE_0:def 5; :: thesis: verum

then |.p.| = 1 by TOPREAL9:12;

hence xx in Sn by A22, A2; :: thesis: verum

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

proof

Sp c= (P1 `) /\ (Sphere ((0. (TOP-REAL n)),1))
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

then |.p.| = 1 by TOPREAL9:12;

hence xx in Sp by A28, A1; :: thesis: verum

end;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

p in Sphere ((0. (TOP-REAL n)),1)
by A25, XBOOLE_0:def 4;
assume
p . n < 0
; :: thesis: contradiction

then p in P1 by A26;

hence contradiction by A27, A24, XBOOLE_0:def 5; :: thesis: verum

end;then p in P1 by A26;

hence contradiction by A27, A24, XBOOLE_0:def 5; :: thesis: verum

then |.p.| = 1 by TOPREAL9:12;

hence xx in Sp by A28, A1; :: thesis: verum

proof

hence
( Sp is closed & Sn is closed )
by A10, A17, XBOOLE_0:def 10, A23; :: thesis: verum
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

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;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

P1 ` = ([#] (TOP-REAL n)) \ P1
by SUBSET_1:def 4;
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;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

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