for a, b, r, s being Real holds closed_inside_of_rectangle (a,b,r,s) = product ((1,2) --> ([.a,b.],[.r,s.]))