for P being Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) holds
( (North-Bound (p,P)) `1 = p `1 & (South-Bound (p,P)) `1 = p `1 ) by EUCLID:52;