theorem :: SPPOL_2:54

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 ) ) }