let a, b, r, s be Real; :: thesis: ( a <= b & r <= s implies not Trectangle (a,b,r,s) is empty )
assume ( a <= b & r <= s ) ; :: thesis: not Trectangle (a,b,r,s) is empty
then |[a,r]| in closed_inside_of_rectangle (a,b,r,s) by Th31;
hence not the carrier of (Trectangle (a,b,r,s)) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum