let T be non empty TopSpace; :: thesis: for A, B being Subset of T st A,B are_separated holds

Fr (A \/ B) = (Fr A) \/ (Fr B)

let A, B be Subset of T; :: thesis: ( A,B are_separated implies Fr (A \/ B) = (Fr A) \/ (Fr B) )

A1: ( (Fr A) \/ (Fr B) = ((Fr (A \/ B)) \/ (Fr (A /\ B))) \/ ((Fr A) /\ (Fr B)) & Fr ({} T) = {} ) by TOPS_1:36;

assume A2: A,B are_separated ; :: thesis: Fr (A \/ B) = (Fr A) \/ (Fr B)

then A3: A misses Cl B by CONNSP_1:def 1;

A misses B by A2, CONNSP_1:1;

then A4: A /\ B = {} ;

A5: Cl A misses B by A2, CONNSP_1:def 1;

A6: (Fr A) \/ (Fr B) c= Fr (A \/ B)

hence Fr (A \/ B) = (Fr A) \/ (Fr B) by A6; :: thesis: verum

Fr (A \/ B) = (Fr A) \/ (Fr B)

let A, B be Subset of T; :: thesis: ( A,B are_separated implies Fr (A \/ B) = (Fr A) \/ (Fr B) )

A1: ( (Fr A) \/ (Fr B) = ((Fr (A \/ B)) \/ (Fr (A /\ B))) \/ ((Fr A) /\ (Fr B)) & Fr ({} T) = {} ) by TOPS_1:36;

assume A2: A,B are_separated ; :: thesis: Fr (A \/ B) = (Fr A) \/ (Fr B)

then A3: A misses Cl B by CONNSP_1:def 1;

A misses B by A2, CONNSP_1:1;

then A4: A /\ B = {} ;

A5: Cl A misses B by A2, CONNSP_1:def 1;

A6: (Fr A) \/ (Fr B) c= Fr (A \/ B)

proof

Fr (A \/ B) c= (Fr A) \/ (Fr B)
by TOPS_1:33;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Fr A) \/ (Fr B) or x in Fr (A \/ B) )

assume A7: x in (Fr A) \/ (Fr B) ; :: thesis: x in Fr (A \/ B)

end;assume A7: x in (Fr A) \/ (Fr B) ; :: thesis: x in Fr (A \/ B)

per cases
( x in Fr (A \/ B) or x in (Fr A) /\ (Fr B) )
by A4, A1, A7, XBOOLE_0:def 3;

end;

suppose A8:
x in (Fr A) /\ (Fr B)
; :: thesis: x in Fr (A \/ B)

then
x in Fr B
by XBOOLE_0:def 4;

then x in (Cl B) /\ (Cl (B `)) by TOPS_1:def 2;

then x in Cl B by XBOOLE_0:def 4;

then not x in A by A3, XBOOLE_0:3;

then A9: x in A ` by A7, XBOOLE_0:def 5;

x in Fr A by A8, XBOOLE_0:def 4;

then x in (Cl A) /\ (Cl (A `)) by TOPS_1:def 2;

then A10: x in Cl A by XBOOLE_0:def 4;

then x in (Cl A) \/ (Cl B) by XBOOLE_0:def 3;

then A11: x in Cl (A \/ B) by PRE_TOPC:20;

not x in B by A5, A10, XBOOLE_0:3;

then x in B ` by A7, XBOOLE_0:def 5;

then x in (A `) /\ (B `) by A9, XBOOLE_0:def 4;

then A12: x in (A \/ B) ` by XBOOLE_1:53;

(A \/ B) ` c= Cl ((A \/ B) `) by PRE_TOPC:18;

then x in (Cl (A \/ B)) /\ (Cl ((A \/ B) `)) by A11, A12, XBOOLE_0:def 4;

hence x in Fr (A \/ B) by TOPS_1:def 2; :: thesis: verum

end;then x in (Cl B) /\ (Cl (B `)) by TOPS_1:def 2;

then x in Cl B by XBOOLE_0:def 4;

then not x in A by A3, XBOOLE_0:3;

then A9: x in A ` by A7, XBOOLE_0:def 5;

x in Fr A by A8, XBOOLE_0:def 4;

then x in (Cl A) /\ (Cl (A `)) by TOPS_1:def 2;

then A10: x in Cl A by XBOOLE_0:def 4;

then x in (Cl A) \/ (Cl B) by XBOOLE_0:def 3;

then A11: x in Cl (A \/ B) by PRE_TOPC:20;

not x in B by A5, A10, XBOOLE_0:3;

then x in B ` by A7, XBOOLE_0:def 5;

then x in (A `) /\ (B `) by A9, XBOOLE_0:def 4;

then A12: x in (A \/ B) ` by XBOOLE_1:53;

(A \/ B) ` c= Cl ((A \/ B) `) by PRE_TOPC:18;

then x in (Cl (A \/ B)) /\ (Cl ((A \/ B) `)) by A11, A12, XBOOLE_0:def 4;

hence x in Fr (A \/ B) by TOPS_1:def 2; :: thesis: verum

hence Fr (A \/ B) = (Fr A) \/ (Fr B) by A6; :: thesis: verum