theorem :: PSCOMP_1:26

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