let T be TopSpace; :: thesis: for A, B being Subset of T
for F being Subset of (T | A) st F = B /\ A holds
Fr F c= (Fr B) /\ A
let A, B 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 5;
[#] (T | A) c= [#] T by PRE_TOPC:def 4;
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:19, 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:17;
[#] (T | A) = A by PRE_TOPC:def 5;
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:19;
then A4: (Cl Fd) /\ A c= (Cl (B `)) /\ A by XBOOLE_1:26;
Cl (F `) = (Cl Fd) /\ ([#] (T | A)) by PRE_TOPC:17;
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