let a, c, b, d be real number ; :: thesis: ( a <= c & b <= d & c <= b implies ( Closed-Interval-TSpace a,d = (Closed-Interval-TSpace a,b) union (Closed-Interval-TSpace c,d) & Closed-Interval-TSpace c,b = (Closed-Interval-TSpace a,b) meet (Closed-Interval-TSpace c,d) ) )
assume A1: ( a <= c & b <= d & c <= b ) ; :: thesis: ( Closed-Interval-TSpace a,d = (Closed-Interval-TSpace a,b) union (Closed-Interval-TSpace c,d) & Closed-Interval-TSpace c,b = (Closed-Interval-TSpace a,b) meet (Closed-Interval-TSpace c,d) )
then A2: ( a <= b & c <= d ) by XXREAL_0:2;
A3: ( the carrier of (Closed-Interval-TSpace a,b) = [.a,b.] & the carrier of (Closed-Interval-TSpace c,d) = [.c,d.] ) by A1, TOPMETR:25, XXREAL_0:2;
A4: the carrier of (Closed-Interval-TSpace a,d) = [.a,d.] by A1, A2, TOPMETR:25, XXREAL_0:2;
[.a,b.] \/ [.c,d.] = [.a,d.] by A1, XXREAL_1:174;
hence Closed-Interval-TSpace a,d = (Closed-Interval-TSpace a,b) union (Closed-Interval-TSpace c,d) by A3, A4, TSEP_1:def 2; :: thesis: Closed-Interval-TSpace c,b = (Closed-Interval-TSpace a,b) meet (Closed-Interval-TSpace c,d)
A5: the carrier of (Closed-Interval-TSpace c,b) = [.c,b.] by A1, TOPMETR:25;
A6: [.a,b.] /\ [.c,d.] = [.c,b.] by A1, XXREAL_1:143;
then the carrier of (Closed-Interval-TSpace a,b) /\ the carrier of (Closed-Interval-TSpace c,d) <> {} by A1, A3, XXREAL_1:1;
then the carrier of (Closed-Interval-TSpace a,b) meets the carrier of (Closed-Interval-TSpace c,d) by XBOOLE_0:def 7;
then Closed-Interval-TSpace a,b meets Closed-Interval-TSpace c,d by TSEP_1:def 3;
hence Closed-Interval-TSpace c,b = (Closed-Interval-TSpace a,b) meet (Closed-Interval-TSpace c,d) by A3, A5, A6, TSEP_1:def 5; :: thesis: verum