let a, b, r, s be Real; ( a <= b & r <= s implies not Trectangle (a,b,r,s) is empty )
assume
( a <= b & r <= s )
; 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
; STRUCT_0:def 1 verum