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

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