let X be non empty TopSpace; :: thesis: for A1, A2 being Subset of X st A1 \/ A2 = the carrier of X holds
( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is closed & C2 is closed & C is open ) )
let A1, A2 be Subset of X; :: thesis: ( A1 \/ A2 = the carrier of X implies ( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is closed & C2 is closed & C is open ) ) )
assume A1:
A1 \/ A2 = the carrier of X
; :: thesis: ( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is closed & C2 is closed & C is open ) )
thus
( A1,A2 are_weakly_separated implies ex C1, C2, C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is closed & C2 is closed & C is open ) )
:: thesis: ( ex C1, C2, C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is closed & C2 is closed & C is open ) implies A1,A2 are_weakly_separated )proof
assume
A1,
A2 are_weakly_separated
;
:: thesis: ex C1, C2, C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is closed & C2 is closed & C is open )
then consider C1,
C2,
C being
Subset of
X such that A2:
(
C1 /\ (A1 \/ A2) c= A1 &
C2 /\ (A1 \/ A2) c= A2 &
C /\ (A1 \/ A2) c= A1 /\ A2 )
and A3:
the
carrier of
X = (C1 \/ C2) \/ C
and A4:
(
C1 is
closed &
C2 is
closed &
C is
open )
by Th59;
take
C1
;
:: thesis: ex C2, C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is closed & C2 is closed & C is open )
take
C2
;
:: thesis: ex C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is closed & C2 is closed & C is open )
take
C
;
:: thesis: ( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is closed & C2 is closed & C is open )
thus
(
A1 \/ A2 = (C1 \/ C2) \/ C &
C1 c= A1 &
C2 c= A2 &
C c= A1 /\ A2 &
C1 is
closed &
C2 is
closed &
C is
open )
by A1, A2, A3, A4, XBOOLE_1:28;
:: thesis: verum
end;
given C1, C2, C being Subset of X such that A5:
A1 \/ A2 = (C1 \/ C2) \/ C
and
A6:
( C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 )
and
A7:
( C1 is closed & C2 is closed & C is open )
; :: thesis: A1,A2 are_weakly_separated
ex C1, C2, C being Subset of X st
( C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C & C1 is closed & C2 is closed & C is open )
hence
A1,A2 are_weakly_separated
by Th59; :: thesis: verum