let C be non empty compact Subset of (TOP-REAL 2); :: thesis: ( C is horizontal iff S-bound C = N-bound C )
thus ( C is horizontal implies S-bound C = N-bound C ) :: thesis: ( S-bound C = N-bound C implies C is horizontal )

proof

assume A1: C is horizontal ; :: thesis: S-bound C = N-bound C
A2: ( S-min C in C & N-min C in C ) by Th13, Th14;
thus S-bound C = (S-min C) `2 by EUCLID:56
.= (N-min C) `2 by A1, A2, SPPOL_1:def 2
.= N-bound C by EUCLID:56 ; :: thesis: verum

end;

assume A3: S-bound C = N-bound C ; :: thesis: C is horizontal
let p be Point of (TOP-REAL 2); :: according to SPPOL_1:def 2 :: thesis: for b₁ being Element of the carrier of (TOP-REAL 2) holds
( not p in C or not b₁ in C or p `2 = b<sub>1</sub> `2 )
let q be Point of (TOP-REAL 2); :: thesis: ( not p in C or not q in C or p `2 = q `2 )
assume ( p in C & q in C ) ; :: thesis: p `2 = q `2
then ( S-bound C <= p `2 & p `2 <= N-bound C & S-bound C <= q `2 & q `2 <= N-bound C ) by PSCOMP_1:71;
then ( p `2 = S-bound C & q `2 = S-bound C ) by A3, XXREAL_0:1;
hence p `2 = q `2 ; :: thesis: verum