let A, B be non empty Interval; :: thesis: ( A is open_interval & B is open_interval & A \/ B is Interval implies ( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) ) )
assume that
A1: A is open_interval and
A2: B is open_interval and
A3: A \/ B is Interval ; :: thesis: ( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) )
ex a1, a2 being R_eal st A = ].a1,a2.[ by A1, MEASURE5:def 2;
then A4: A = ].(inf A),(sup A).[ by XXREAL_2:78;
ex b1, b2 being R_eal st B = ].b1,b2.[ by A2, MEASURE5:def 2;
then A5: B = ].(inf B),(sup B).[ by XXREAL_2:78;
A6: inf (A \/ B) = min ((inf A),(inf B)) by XXREAL_2:9;
A7: sup (A \/ B) = max ((sup A),(sup B)) by XXREAL_2:10;

per cases ( inf A <= inf B or inf A > inf B ) ;

suppose A8: inf A <= inf B ; :: thesis: ( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) )

then A9: inf (A \/ B) = inf A by A6, XXREAL_0:def 9;

per cases ( sup A <= sup B or sup A > sup B ) ;

suppose A10: sup A <= sup B ; :: thesis: ( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) )

then A11: A \/ B = ].(inf A),(sup B).[ \ [.(sup A),(inf B).] by A4, A5, A8, XXREAL_1:309;
A12: sup (A \/ B) = sup B by A7, A10, XXREAL_0:def 10;

A13: now :: thesis: not sup A <= inf B

assume sup A <= inf B ; :: thesis: contradiction
then not [.(sup A),(inf B).] is empty by XXREAL_1:30;
then consider x being ExtReal such that
A14: x in [.(sup A),(inf B).] by MEMBERED:8;
( sup A <= x & x <= inf B ) by A14, XXREAL_1:1;
then ( inf A < x & x < sup B ) by A4, A5, XXREAL_1:28, XXREAL_0:2;
then x in A \/ B by A3, A9, A12, XXREAL_2:83;
hence contradiction by A11, A14, XBOOLE_0:def 5; :: thesis: verum

end;

then [.(sup A),(inf B).] = {} by XXREAL_1:29;
hence A \/ B is open_interval by A11, MEASURE5:def 2; :: thesis: ( A meets B & ( inf A < sup B or inf B < sup A ) )
].(inf B),(sup A).[ <> {} by A13, XXREAL_1:33;
then consider y being ExtReal such that
A15: y in ].(inf B),(sup A).[ by MEMBERED:8;
( inf B < y & y < sup A ) by A15, XXREAL_1:4;
then ( inf A < y & y < sup A & inf B < y & y < sup B ) by A8, A10, XXREAL_0:2;
then ( y in A & y in B ) by A4, A5, XXREAL_1:4;
hence A meets B by XBOOLE_0:3; :: thesis: ( inf A < sup B or inf B < sup A )
thus ( inf A < sup B or inf B < sup A ) by A13; :: thesis: verum

end;

suppose sup A > sup B ; :: thesis: ( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) )

hence ( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) ) by A1, A4, A5, A8, XXREAL_1:28, XXREAL_1:46, XBOOLE_1:12, XBOOLE_1:69, XXREAL_0:2; :: thesis: verum

end;

end;

end;

suppose A16: inf A > inf B ; :: thesis: ( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) )

then A17: inf (A \/ B) = inf B by A6, XXREAL_0:def 9;

per cases ( sup A <= sup B or sup A > sup B ) ;

suppose sup A <= sup B ; :: thesis: ( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) )

hence ( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) ) by A2, A4, A5, A16, XXREAL_1:28, XXREAL_1:46, XBOOLE_1:12, XBOOLE_1:69, XXREAL_0:2; :: thesis: verum

end;

suppose A18: sup A > sup B ; :: thesis: ( A \/ B is open_interval & A meets B & ( inf A < sup B or inf B < sup A ) )

then A19: A \/ B = ].(inf B),(sup A).[ \ [.(sup B),(inf A).] by A4, A5, A16, XXREAL_1:309;
A20: sup (A \/ B) = sup A by A7, A18, XXREAL_0:def 10;

A21: now :: thesis: not sup B <= inf A

assume sup B <= inf A ; :: thesis: contradiction
then not [.(sup B),(inf A).] is empty by XXREAL_1:30;
then consider x being ExtReal such that
A22: x in [.(sup B),(inf A).] by MEMBERED:8;
( sup B <= x & x <= inf A ) by A22, XXREAL_1:1;
then ( inf B < x & x < sup A ) by A4, A5, XXREAL_1:28, XXREAL_0:2;
then x in A \/ B by A3, A17, A20, XXREAL_2:83;
hence contradiction by A19, A22, XBOOLE_0:def 5; :: thesis: verum

end;

then [.(sup B),(inf A).] = {} by XXREAL_1:29;
hence A \/ B is open_interval by A19, MEASURE5:def 2; :: thesis: ( A meets B & ( inf A < sup B or inf B < sup A ) )
].(inf A),(sup B).[ <> {} by A21, XXREAL_1:33;
then consider y being ExtReal such that
A23: y in ].(inf A),(sup B).[ by MEMBERED:8;
( inf A < y & y < sup B ) by A23, XXREAL_1:4;
then ( inf B < y & y < sup B & inf A < y & y < sup A ) by A16, A18, XXREAL_0:2;
then ( y in A & y in B ) by A4, A5, XXREAL_1:4;
hence A meets B by XBOOLE_0:3; :: thesis: ( inf A < sup B or inf B < sup A )
thus ( inf A < sup B or inf B < sup A ) by A21; :: thesis: verum

end;

end;

end;

end;