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

assume that

A1: a <= b and

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

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

A3: 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 12;

W-bound (rectangle (a,b,c,d)) = a by A1, A2, Th36;

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

assume that

A1: a <= b and

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

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

A3: 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 12;

W-bound (rectangle (a,b,c,d)) = a by A1, A2, Th36;

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