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