let T be non empty TopSpace; :: thesis: for V being Subset of T
for FX being Subset-Family of T st FX = {V} holds
clf FX = {(Cl V)}
let V be Subset of T; :: thesis: for FX being Subset-Family of T st FX = {V} holds
clf FX = {(Cl V)}
let FX be Subset-Family of T; :: thesis: ( FX = {V} implies clf FX = {(Cl V)} )
reconsider CFX = clf FX as set ;
assume A1: FX = {V} ; :: thesis: clf FX = {(Cl V)}
for W being object holds
( W in CFX iff W = Cl V )
proof
let W be object ; :: thesis: ( W in CFX iff W = Cl V )
A2: ( W = Cl V implies W in CFX )
proof
assume A3: W = Cl V ; :: thesis: W in CFX
ex X being Subset of T st
( W = Cl X & X in FX )
proof
take V ; :: thesis: ( W = Cl V & V in FX )
thus ( W = Cl V & V in FX ) by A1, A3, TARSKI:def 1; :: thesis: verum
end;
hence W in CFX by Def2; :: thesis: verum
end;
( W in CFX implies W = Cl V )
proof
assume A4: W in CFX ; :: thesis: W = Cl V
then reconsider W = W as Subset of T ;
ex X being Subset of T st
( W = Cl X & X in FX ) by A4, Def2;
hence W = Cl V by A1, TARSKI:def 1; :: thesis: verum
end;
hence ( W in CFX iff W = Cl V ) by A2; :: thesis: verum
end;
hence clf FX = {(Cl V)} by TARSKI:def 1; :: thesis: verum