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 that
A1: A,B are_separated and
A2: A,C are_separated ; :: thesis: A,B \/ C are_separated
A3: A ^b misses C by A2, FINTOPO4:def 1;
A ^b misses B by A1, FINTOPO4:def 1;
then A4: (A ^b) /\ B = {} ;
(A ^b) /\ (B \/ C) = ((A ^b) /\ B) \/ ((A ^b) /\ C) by XBOOLE_1:23
.= {} by A3, A4 ;
then A5: A ^b misses B \/ C ;
A misses B ^b by A1, FINTOPO4:def 1;
then A6: A /\ (B ^b) = {} ;
A7: A misses C ^b by A2, FINTOPO4:def 1;
A /\ ((B \/ C) ^b) = A /\ ((B ^b) \/ (C ^b)) by FINTOPO3:8
.= (A /\ (B ^b)) \/ (A /\ (C ^b)) by XBOOLE_1:23
.= {} by A7, A6 ;
then A misses (B \/ C) ^b ;
hence A,B \/ C are_separated by A5, FINTOPO4:def 1; :: thesis: verum