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 open & C2 is open & C is closed ) )
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 open & C2 is open & C is closed ) ) )
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 open & C2 is open & C is closed ) )
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 open & C2 is open & C is closed ) ) :: 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 open & C2 is open & C is closed ) 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 open & C2 is open & C is closed )
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 & the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed ) by Th58;
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 open & C2 is open & C is closed )
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 open & C2 is open & C is closed )
take C ; :: thesis: ( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is open & C2 is open & C is closed )
thus ( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is open & C2 is open & C is closed ) by A1, A2, XBOOLE_1:28; :: thesis: verum

end;

given C1, C2, C being Subset of X such that A3: ( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is open & C2 is open & C is closed ) ; :: 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 open & C2 is open & C is closed )

proof

take C1 ; :: thesis: ex 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 open & C2 is open & C is closed )
take C2 ; :: thesis: ex 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 open & C2 is open & C is closed )
take C ; :: thesis: ( 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 open & C2 is open & C is closed )
thus ( 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 open & C2 is open & C is closed ) by A1, A3, XBOOLE_1:28; :: thesis: verum

end;

hence A1,A2 are_weakly_separated by Th58; :: thesis: verum