for P, Q being Element of (TOP-REAL 2) holds
( not P <> Q or P . 1 <> Q . 1 or P . 2 <> Q . 2 )