let FT be non empty RelStr ; :: thesis: for A, B, C being Subset of FT st A,B are_separated & A,C are_separated holds
A,B \/ C are_separated
let A, B, C be Subset of FT; :: thesis: ( A,B are_separated & A,C are_separated implies A,B \/ C are_separated )
assume A1: ( A,B are_separated & A,C are_separated ) ; :: thesis: A,B \/ C are_separated
then A2: ( A ^b misses B & A misses B ^b ) by FINTOPO4:def 1;
( A ^b misses C & A misses C ^b ) by A1, FINTOPO4:def 1;
then A3: ( (A ^b ) /\ B = {} & A /\ (B ^b ) = {} & (A ^b ) /\ C = {} & A /\ (C ^b ) = {} ) by A2, XBOOLE_0:def 7;
(A ^b ) /\ (B \/ C) = ((A ^b ) /\ B) \/ ((A ^b ) /\ C) by XBOOLE_1:23
.= {} by A3 ;
then A4: A ^b misses B \/ C by XBOOLE_0:def 7;
A /\ ((B \/ C) ^b ) = A /\ ((B ^b ) \/ (C ^b )) by Th1
.= (A /\ (B ^b )) \/ (A /\ (C ^b )) by XBOOLE_1:23
.= {} by A3 ;
then A misses (B \/ C) ^b by XBOOLE_0:def 7;
hence A,B \/ C are_separated by A4, FINTOPO4:def 1; :: thesis: verum