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