let FT be non empty RelStr ; 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; ( 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
; 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 = {}
by XBOOLE_0:def 7;
(A ^b) /\ (B \/ C) =
((A ^b) /\ B) \/ ((A ^b) /\ C)
by XBOOLE_1:23
.=
{}
by A3, A4, XBOOLE_0:def 7
;
then A5:
A ^b misses B \/ C
by XBOOLE_0:def 7;
A misses B ^b
by A1, FINTOPO4:def 1;
then A6:
A /\ (B ^b) = {}
by XBOOLE_0:def 7;
A7:
A misses C ^b
by A2, FINTOPO4:def 1;
A /\ ((B \/ C) ^b) =
A /\ ((B ^b) \/ (C ^b))
by Th1
.=
(A /\ (B ^b)) \/ (A /\ (C ^b))
by XBOOLE_1:23
.=
{}
by A7, A6, XBOOLE_0:def 7
;
then
A misses (B \/ C) ^b
by XBOOLE_0:def 7;
hence
A,B \/ C are_separated
by A5, FINTOPO4:def 1; verum