let a, b, c, d be real number ; :: 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 34;
A6: NW-corner (rectangle a,b,c,d) = |[a,d]| by A1, A2, Th50;
A7: W-bound (rectangle a,b,c,d) = a by A1, A2, Th46;
A8: S-bound (rectangle a,b,c,d) = c by A1, A2, Th49;
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 38
.= LSeg |[a,c]|,|[a,d]| by A3, A4, A5, A6, A7, A8, XBOOLE_1:1, XBOOLE_1:28 ; :: thesis: verum