let a, b, c, d be Real; :: thesis: ( a <= b & c <= d implies SW-corner (rectangle (a,b,c,d)) = |[a,c]| )
set K = rectangle (a,b,c,d);
assume that
A1: a <= b and
A2: c <= d ; :: thesis: SW-corner (rectangle (a,b,c,d)) = |[a,c]|
A3: SW-corner (rectangle (a,b,c,d)) = |[(W-bound (rectangle (a,b,c,d))),(S-bound (rectangle (a,b,c,d)))]| by PSCOMP_1:def 11;
W-bound (rectangle (a,b,c,d)) = a by A1, A2, Th36;
hence SW-corner (rectangle (a,b,c,d)) = |[a,c]| by A1, A2, A3, Th39; :: thesis: verum