let T be non empty TopSpace; :: thesis:
let FX be Subset-Family of T; :: thesis:
set GX = clf FX;
for X being set st X in FX holds
ex Y being set st
( Y in clf FX & X c= Y )

let X be set ; :: thesis:
assume A1: X in FX ; :: thesis:
then reconsider X = X as Subset of T ;
thus ex Y being set st
( Y in clf FX & X c= Y ) :: thesis:

reconsider Y = Cl X as set ;
take Y ; :: thesis:
thus Y in clf FX by A1, Def2; :: thesis:
thus X c= Y by PRE_TOPC:18; :: thesis:

end;