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 & the carrier of X = (C1 \/ C2) \/ C & C1 is closed & C2 is closed & C is open ) by Th54;
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, 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 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 )
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 closed & C2 is closed & C is open )
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 closed & C2 is closed & C is open )
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 closed & C2 is closed & C is open )
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 closed & C2 is closed & C is open ) by A1, A3, XBOOLE_1:28; :: thesis: verum
end;
hence A1,A2 are_weakly_separated by Th54; :: thesis: verum