let P be Subset of (TOP-REAL 2); :: thesis: ( (SE-corner P) `1 = (E-min P) `1 & (SE-corner P) `1 = (E-max P) `1 & (E-min P) `1 = (E-max P) `1 & (E-min P) `1 = (NE-corner P) `1 & (E-max P) `1 = (NE-corner P) `1 )
( (E-min P) `1 = E-bound P & (E-max P) `1 = E-bound P ) by EUCLID:52;
hence ( (SE-corner P) `1 = (E-min P) `1 & (SE-corner P) `1 = (E-max P) `1 & (E-min P) `1 = (E-max P) `1 & (E-min P) `1 = (NE-corner P) `1 & (E-max P) `1 = (NE-corner P) `1 ) by EUCLID:52; :: thesis: verum