let I, J be Subset of REAL; ( I is closed_interval & J is closed_interval & I meets J implies ex K, L being Interval st
( K misses L & I \ J = K \/ L ) )
assume A1:
( I is closed_interval & J is closed_interval & I meets J )
; ex K, L being Interval st
( K misses L & I \ J = K \/ L )
then consider p, q being Real such that
A2:
I = [.p,q.]
;
consider r, s being Real such that
A3:
J = [.r,s.]
by A1;
( I <> {} & J <> {} )
by A1;
then A4:
( p <= q & r <= s & p <= s & r <= q )
by A1, A2, A3, XXREAL_1:29, XXREAL_1:278;
reconsider K = [.p,r.[, L = ].s,q.] as Subset of REAL ;
( r is R_eal & s is R_eal )
by XXREAL_0:def 1;
then
( K is right_open_interval & L is left_open_interval )
;
then reconsider K = K, L = L as Interval ;
take
K
; ex L being Interval st
( K misses L & I \ J = K \/ L )
take
L
; ( K misses L & I \ J = K \/ L )
thus
( K misses L & I \ J = K \/ L )
by A4, A2, A3, XXREAL_1:312, XXREAL_1:274; verum