let I, J be Subset of REAL; :: thesis: ( I is right_open_interval & J is right_open_interval & I meets J implies ex K, L being Interval st
( K misses L & I \ J = K \/ L ) )
assume ( I is right_open_interval & J is right_open_interval & I meets J ) ; :: thesis: ex K, L being Interval st
( K misses L & I \ J = K \/ L )
then consider K, L being Subset of REAL such that
A2: ( K is right_open_interval & L is right_open_interval & K misses L & I \ J = K \/ L ) by INTERVAL02;
reconsider K = K, L = L as Interval by A2;
thus ex K, L being Interval st
( K misses L & I \ J = K \/ L ) by A2; :: thesis: verum