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)

proof

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)

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

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

hence x in Fr (A \/ B) ; :: thesis: verum

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;

end;

end;

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