theorem :: PSCOMP_1:27

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