let T1, T2 be TopSpace; :: thesis: for A1 being Subset of T1
for A2 being Subset of T2 holds Fr [:A1,A2:] = [:(Fr A1),(Cl A2):] \/ [:(Cl A1),(Fr A2):]
let A1 be Subset of T1; :: thesis: for A2 being Subset of T2 holds Fr [:A1,A2:] = [:(Fr A1),(Cl A2):] \/ [:(Cl A1),(Fr A2):]
let A2 be Subset of T2; :: thesis: Fr [:A1,A2:] = [:(Fr A1),(Cl A2):] \/ [:(Cl A1),(Fr A2):]
A1: [:(Cl A1),(Cl A2):] /\ [:(Cl (A1 `)),([#] T2):] = [:((Cl A1) /\ (Cl (A1 `))),((Cl A2) /\ ([#] T2)):] by ZFMISC_1:100
.= [:(Fr A1),(Cl A2):] by XBOOLE_1:28 ;
A2: [:(Cl A1),(Cl A2):] /\ [:([#] T1),(Cl (A2 `)):] = [:((Cl A1) /\ ([#] T1)),((Cl A2) /\ (Cl (A2 `))):] by ZFMISC_1:100
.= [:(Cl A1),(Fr A2):] by XBOOLE_1:28 ;
Cl ([#] T1) = [#] T1 by TOPS_1:2;
then A3: Cl [:([#] T1),(A2 `):] = [:([#] T1),(Cl (A2 `)):] by TOPALG_3:14;
Cl ([#] T2) = [#] T2 by TOPS_1:2;
then A4: Cl [:(A1 `),([#] T2):] = [:(Cl (A1 `)),([#] T2):] by TOPALG_3:14;
Cl ([:A1,A2:] `) = Cl ([:([#] T1),([#] T2):] \ [:A1,A2:]) by BORSUK_1:def 2
.= Cl ([:(([#] T1) \ A1),([#] T2):] \/ [:([#] T1),(([#] T2) \ A2):]) by ZFMISC_1:103
.= [:(Cl (A1 `)),([#] T2):] \/ [:([#] T1),(Cl (A2 `)):] by A4, A3, PRE_TOPC:20 ;
hence Fr [:A1,A2:] = [:(Cl A1),(Cl A2):] /\ ([:(Cl (A1 `)),([#] T2):] \/ [:([#] T1),(Cl (A2 `)):]) by TOPALG_3:14
.= [:(Fr A1),(Cl A2):] \/ [:(Cl A1),(Fr A2):] by A1, A2, XBOOLE_1:23 ;
:: thesis: verum