let C be non empty compact Subset of (TOP-REAL 2); :: thesis: ( C is vertical iff W-bound C = E-bound C )
thus ( C is vertical implies W-bound C = E-bound C ) :: thesis: ( W-bound C = E-bound C implies C is vertical )

proof

assume A1: C is vertical ; :: thesis: W-bound C = E-bound C
A2: ( W-min C in C & E-min C in C ) by Th15, Th16;
thus W-bound C = (W-min C) `1 by EUCLID:56
.= (E-min C) `1 by A1, A2, SPPOL_1:def 3
.= E-bound C by EUCLID:56 ; :: thesis: verum

end;

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