let a, b, r, s be real number ; :: thesis: ( a <= b & r <= s implies |[a,r]| in closed_inside_of_rectangle a,b,r,s )
set o = |[a,r]|;
assume A1: ( a <= b & r <= s ) ; :: thesis: |[a,r]| in closed_inside_of_rectangle a,b,r,s
A2: closed_inside_of_rectangle a,b,r,s = { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & r <= p `2 & p `2 <= s ) } by JGRAPH_6:def 2;
( |[a,r]| `1 = a & |[a,r]| `2 = r ) by EUCLID:56;
hence |[a,r]| in closed_inside_of_rectangle a,b,r,s by A1, A2; :: thesis: verum