let a, b, c, d be real number ; :: thesis: ( a <= b & c <= d implies NE-corner (rectangle a,b,c,d) = |[b,d]| )
set K = rectangle a,b,c,d;
assume that
A1: a <= b and
A2: c <= d ; :: thesis: NE-corner (rectangle a,b,c,d) = |[b,d]|
A3: NE-corner (rectangle a,b,c,d) = |[(E-bound (rectangle a,b,c,d)),(N-bound (rectangle a,b,c,d))]| by PSCOMP_1:def 36;
E-bound (rectangle a,b,c,d) = b by A1, A2, Th48;
hence NE-corner (rectangle a,b,c,d) = |[b,d]| by A1, A2, A3, Th47; :: thesis: verum