let r1, r2, s1, s2 be Real; :: thesis: ( r1 < r2 & s1 < s2 implies [.r1,r2,s1,s2.] is Jordan )
assume that
A1: r1 < r2 and
A2: s1 < s2 ; :: thesis: [.r1,r2,s1,s2.] is Jordan
[.r1,r2,s1,s2.] = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= s2 & p `2 >= s1 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = s2 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = s1 ) or ( p `1 = r2 & p `2 <= s2 & p `2 >= s1 ) ) } by A1, A2, SPPOL_2:54;
hence [.r1,r2,s1,s2.] is Jordan by A1, A2, JORDAN1:43; :: thesis: verum