let GX be non empty TopSpace; :: thesis: for B being Subset of GX

for V being Subset of (GX | B) holds Cl V = (Cl (Up V)) /\ B

let B be Subset of GX; :: thesis: for V being Subset of (GX | B) holds Cl V = (Cl (Up V)) /\ B

let V be Subset of (GX | B); :: thesis: Cl V = (Cl (Up V)) /\ B

A1: B = [#] (GX | B) by PRE_TOPC:def 5;

then Cl (Down ((Up V),B)) = (Cl (Up V)) /\ B by Th29;

hence Cl V = (Cl (Up V)) /\ B by A1, XBOOLE_1:28; :: thesis: verum

for V being Subset of (GX | B) holds Cl V = (Cl (Up V)) /\ B

let B be Subset of GX; :: thesis: for V being Subset of (GX | B) holds Cl V = (Cl (Up V)) /\ B

let V be Subset of (GX | B); :: thesis: Cl V = (Cl (Up V)) /\ B

A1: B = [#] (GX | B) by PRE_TOPC:def 5;

then Cl (Down ((Up V),B)) = (Cl (Up V)) /\ B by Th29;

hence Cl V = (Cl (Up V)) /\ B by A1, XBOOLE_1:28; :: thesis: verum