let T be TopSpace; :: thesis: for B, A being Subset of T
for F being Subset of (T | A) st F = B /\ A holds
Fr F c= (Fr B) /\ A
let B, A be Subset of T; :: thesis: for F being Subset of (T | A) st F = B /\ A holds
Fr F c= (Fr B) /\ A
let F be Subset of (T | A); :: thesis: ( F = B /\ A implies Fr F c= (Fr B) /\ A )
A1: [#] (T | A) = A by PRE_TOPC:def 10;
[#] (T | A) c= [#] T by PRE_TOPC:def 9;
then reconsider F9 = F, Fd = F ` as Subset of T by XBOOLE_1:1;
assume A2: F = B /\ A ; :: thesis: Fr F c= (Fr B) /\ A
then Cl F9 c= Cl B by PRE_TOPC:49, XBOOLE_1:18;
then (Cl F9) /\ A c= (Cl B) /\ A by XBOOLE_1:26;
then A3: Cl F c= (Cl B) /\ A by A1, PRE_TOPC:47;
[#] (T | A) = A by PRE_TOPC:def 10;
then F ` = A \ B by A2, XBOOLE_1:47;
then F ` c= B ` by XBOOLE_1:35;
then Cl Fd c= Cl (B ` ) by PRE_TOPC:49;
then A4: (Cl Fd) /\ A c= (Cl (B ` )) /\ A by XBOOLE_1:26;
Cl (F ` ) = (Cl Fd) /\ ([#] (T | A)) by PRE_TOPC:47;
then Cl (F ` ) c= Cl (B ` ) by A1, A4, XBOOLE_1:18;
then (Cl F) /\ (Cl (F ` )) c= ((Cl B) /\ A) /\ (Cl (B ` )) by A3, XBOOLE_1:27;
hence Fr F c= (Fr B) /\ A by XBOOLE_1:16; :: thesis: verum