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
A1: E-min C in C by Th14;
A2: W-min C in C by Th13;
assume A3: C is vertical ; :: thesis: W-bound C = E-bound C
thus W-bound C = (W-min C) `1 by EUCLID:52
.= (E-min C) `1 by A3, A2, A1
.= E-bound C by EUCLID:52 ; :: thesis: verum
end;
assume A4: 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 b1 being Element of the carrier of (TOP-REAL 2) holds
( not p in C or not b1 in C or p `1 = b1 `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 that
A5: p in C and
A6: q in C ; :: thesis: p `1 = q `1
A7: p `1 <= E-bound C by A5, PSCOMP_1:24;
W-bound C <= p `1 by A5, PSCOMP_1:24;
then A8: p `1 = W-bound C by A4, A7, XXREAL_0:1;
A9: q `1 <= E-bound C by A6, PSCOMP_1:24;
W-bound C <= q `1 by A6, PSCOMP_1:24;
hence p `1 = q `1 by A4, A9, A8, XXREAL_0:1; :: thesis: verum