let a, b, c, d be Real; ( 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
; 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 13;
E-bound (rectangle (a,b,c,d)) = b
by A1, A2, Th38;
hence
NE-corner (rectangle (a,b,c,d)) = |[b,d]|
by A1, A2, A3, Th37; verum