let a, b, c, d be real number ; :: thesis: ( a <= b & c <= d implies NW-corner (rectangle a,b,c,d) = |[a,d]| )
assume A1: ( a <= b & c <= d ) ; :: thesis: NW-corner (rectangle a,b,c,d) = |[a,d]|
set K = rectangle a,b,c,d;
A2: NW-corner (rectangle a,b,c,d) = |[(W-bound (rectangle a,b,c,d)),(N-bound (rectangle a,b,c,d))]| by PSCOMP_1:def 35;
W-bound (rectangle a,b,c,d) = a by A1, Th46;
hence NW-corner (rectangle a,b,c,d) = |[a,d]| by A1, A2, Th47; :: thesis: verum