let a, b, c, d be Real; ( 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:18, 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:18, XXREAL_0:2;
A6:
the carrier of (Closed-Interval-TSpace (c,b)) = [.c,b.]
by A3, TOPMETR:18;
[.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 4; verum