:: deftheorem defines Trectangle TOPREALA:def 1 :
for a, b, c, d being Real holds Trectangle (a,b,c,d) = (TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d));