let p, q be Point of (TOP-REAL 2); :: thesis: ( p `1 = q `1 & p `2 = q `2 implies p = q )
assume ( p `1 = q `1 & p `2 = q `2 ) ; :: thesis: p = q
hence p = |[(q `1),(q `2)]| by EUCLID:53
.= q by EUCLID:53 ;
:: thesis: verum