let P, Q be Element of (TOP-REAL 2); :: thesis: ( not P <> Q or P . 1 <> Q . 1 or P . 2 <> Q . 2 )
assume A1: P <> Q ; :: thesis: ( P . 1 <> Q . 1 or P . 2 <> Q . 2 )
assume ( P . 1 = Q . 1 & P . 2 = Q . 2 ) ; :: thesis: contradiction
then ( P `1 = Q `1 & P `2 = Q `2 ) ;
then P = |[(Q `1),(Q `2)]| by EUCLID:53
.= Q by EUCLID:53 ;
hence contradiction by A1; :: thesis: verum