:: deftheorem defines inside_of_rectangle JGRAPH_6:def 1 :
for a, b, c, d being Real holds 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 ) } ;