let a, b, r, s be real number ; :: 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 Th52;
hence not the carrier of (Trectangle a,b,r,s) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum