let a, b, c, d be Real; :: thesis: ( a <= b & c <= d implies SE-corner (rectangle (a,b,c,d)) = |[b,c]| )

set K = rectangle (a,b,c,d);

assume that

A1: a <= b and

A2: c <= d ; :: thesis: SE-corner (rectangle (a,b,c,d)) = |[b,c]|

A3: SE-corner (rectangle (a,b,c,d)) = |[(E-bound (rectangle (a,b,c,d))),(S-bound (rectangle (a,b,c,d)))]| by PSCOMP_1:def 14;

E-bound (rectangle (a,b,c,d)) = b by A1, A2, Th38;

hence SE-corner (rectangle (a,b,c,d)) = |[b,c]| by A1, A2, A3, Th39; :: thesis: verum

set K = rectangle (a,b,c,d);

assume that

A1: a <= b and

A2: c <= d ; :: thesis: SE-corner (rectangle (a,b,c,d)) = |[b,c]|

A3: SE-corner (rectangle (a,b,c,d)) = |[(E-bound (rectangle (a,b,c,d))),(S-bound (rectangle (a,b,c,d)))]| by PSCOMP_1:def 14;

E-bound (rectangle (a,b,c,d)) = b by A1, A2, Th38;

hence SE-corner (rectangle (a,b,c,d)) = |[b,c]| by A1, A2, A3, Th39; :: thesis: verum