theorem :: PSCOMP_1:25

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