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:57
.= q by EUCLID:57 ;
:: thesis: verum