:: deftheorem defines closed_inside_of_rectangle JGRAPH_6:def 2 :
for a, b, c, d being Real holds closed_inside_of_rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } ;