let T be TopSpace; :: thesis: for FX being Subset-Family of T holds clf FX is closed
let FX be Subset-Family of T; :: thesis: clf FX is closed
for V being Subset of T st V in clf FX holds
V is closed
proof
let V be Subset of T; :: thesis: ( V in clf FX implies V is closed )
assume V in clf FX ; :: thesis: V is closed
then ex W being Subset of T st
( V = Cl W & W in FX ) by Def2;
hence V is closed ; :: thesis: verum
end;
hence clf FX is closed by TOPS_2:def 2; :: thesis: verum