let a, b, r, s be Real; :: thesis: ( a <= b & r <= s implies |[a,r]| in closed_inside_of_rectangle (a,b,r,s) )
set o = |[a,r]|;
A1: ( 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 ) } & |[a,r]| `1 = a ) by EUCLID:52, JGRAPH_6:def 2;
A2: |[a,r]| `2 = r by EUCLID:52;
assume ( a <= b & r <= s ) ; :: thesis: |[a,r]| in closed_inside_of_rectangle (a,b,r,s)
hence |[a,r]| in closed_inside_of_rectangle (a,b,r,s) by A1, A2; :: thesis: verum