let a, b, c, d be real number ; :: thesis: ( a <= b & c <= d implies SE-corner (rectangle a,b,c,d) = |[b,c]| )
set K = rectangle a,b,c,d;
assume A1: ( a <= b & c <= d ) ; :: thesis: SE-corner (rectangle a,b,c,d) = |[b,c]|
A2: 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 37;
E-bound (rectangle a,b,c,d) = b by A1, Th48;
hence SE-corner (rectangle a,b,c,d) = |[b,c]| by A1, A2, Th49; :: thesis: verum