let a, c, b, d be real number ; ( 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 that
A1:
a <= c
and
A2:
b <= d
and
A3:
c <= b
; ( 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) )
A4:
( the carrier of (Closed-Interval-TSpace a,b) = [.a,b.] & the carrier of (Closed-Interval-TSpace c,d) = [.c,d.] )
by A1, A2, A3, TOPMETR:25, XXREAL_0:2;
a <= b
by A1, A3, XXREAL_0:2;
then A5:
the carrier of (Closed-Interval-TSpace a,d) = [.a,d.]
by A2, TOPMETR:25, XXREAL_0:2;
A6:
the carrier of (Closed-Interval-TSpace c,b) = [.c,b.]
by A3, TOPMETR:25;
[.a,b.] \/ [.c,d.] = [.a,d.]
by A1, A2, A3, XXREAL_1:174;
hence
Closed-Interval-TSpace a,d = (Closed-Interval-TSpace a,b) union (Closed-Interval-TSpace c,d)
by A4, A5, TSEP_1:def 2; Closed-Interval-TSpace c,b = (Closed-Interval-TSpace a,b) meet (Closed-Interval-TSpace c,d)
A7:
[.a,b.] /\ [.c,d.] = [.c,b.]
by A1, A2, XXREAL_1:143;
then
the carrier of (Closed-Interval-TSpace a,b) /\ the carrier of (Closed-Interval-TSpace c,d) <> {}
by A3, A4, 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 A4, A6, A7, TSEP_1:def 5; verum