theorem :: PSCOMP_1:28

for P being Subset of (TOP-REAL 2) holds (SW-corner P) `2 = (SE-corner P) `2