for r1, r2, r19, r29 being Real st r1 <= r2 & r19 <= r29 holds [.r1,r2,r19,r29.]= { p where p is Point of (TOP-REAL 2) : ( ( p `1= r1 & p `2<= r29 & p `2>= r19 ) or ( p `1<= r2 & p `1>= r1 & p `2= r29 ) or ( p `1<= r2 & p `1>= r1 & p `2= r19 ) or ( p `1= r2 & p `2<= r29 & p `2>= r19 ) ) }