let a, b, c, d be Real; :: thesis: ( a <= b & c <= d implies W-most (rectangle (a,b,c,d)) = LSeg (|[a,c]|,|[a,d]|) )
set K = rectangle (a,b,c,d);
assume that
A1: a <= b and
A2: c <= d ; :: thesis: W-most (rectangle (a,b,c,d)) = LSeg (|[a,c]|,|[a,d]|)
rectangle (a,b,c,d) = ((LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|))) \/ ((LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|))) by SPPOL_2:def 3;
then A3: (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) c= rectangle (a,b,c,d) by XBOOLE_1:7;
A4: LSeg (|[a,c]|,|[a,d]|) c= (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) by XBOOLE_1:7;
A5: 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;
A6: NW-corner (rectangle (a,b,c,d)) = |[a,d]| by A1, A2, Th40;
A7: W-bound (rectangle (a,b,c,d)) = a by A1, A2, Th36;
A8: S-bound (rectangle (a,b,c,d)) = c by A1, A2, Th39;
thus W-most (rectangle (a,b,c,d)) = (LSeg ((SW-corner (rectangle (a,b,c,d))),(NW-corner (rectangle (a,b,c,d))))) /\ (rectangle (a,b,c,d)) by PSCOMP_1:def 15
.= LSeg (|[a,c]|,|[a,d]|) by A3, A4, A5, A6, A7, A8, XBOOLE_1:1, XBOOLE_1:28 ; :: thesis: verum