let P be Subset of (TOP-REAL 2); for p1, p2, q1 being Point of (TOP-REAL 2) st q1 in P holds
LE q1,q1,P,p1,p2
let p1, p2, q1 be Point of (TOP-REAL 2); ( q1 in P implies LE q1,q1,P,p1,p2 )
assume A1:
q1 in P
; LE q1,q1,P,p1,p2
then reconsider P = P as non empty Subset of (TOP-REAL 2) ;
hence
LE q1,q1,P,p1,p2
by A1; verum