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