let GX be TopSpace; :: thesis: for A being Subset of GX ex F being Subset-Family of GX st
( ( for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )
let A be Subset of GX; :: thesis: ex F being Subset-Family of GX st
( ( for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )
defpred S₁[ set ] means ex C1 being Subset of GX st
( C1 = $1 & C1 is closed & A c= $1 );
consider F9 being Subset-Family of GX such that
A1: for C being Subset of GX holds
( C in F9 iff S₁[C] ) from SUBSET_1:sch 3();
take F = F9; :: thesis: ( ( for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )
thus for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) :: thesis: Cl A = meet F

proof

let C be Subset of GX; :: thesis: ( C in F iff ( C is closed & A c= C ) )
thus ( C in F implies ( C is closed & A c= C ) ) :: thesis: ( C is closed & A c= C implies C in F )

proof

assume C in F ; :: thesis: ( C is closed & A c= C )
then ex C1 being Subset of GX st
( C1 = C & C1 is closed & A c= C ) by A1;
hence ( C is closed & A c= C ) ; :: thesis: verum

end;

thus ( C is closed & A c= C implies C in F ) by A1; :: thesis: verum

end;

A c= [#] GX ;
then A2: F <> {} by A1;
for p being object holds
( p in Cl A iff p in meet F )

proof

let p be object ; :: thesis: ( p in Cl A iff p in meet F )

A3: now :: thesis: ( p in meet F implies p in Cl A )

assume A4: p in meet F ; :: thesis: p in Cl A

now :: thesis: for C being Subset of GX st C is closed & A c= C holds
p in C

let C be Subset of GX; :: thesis: ( C is closed & A c= C implies p in C )
assume ( C is closed & A c= C ) ; :: thesis: p in C
then C in F by A1;
hence p in C by A4, SETFAM_1:def 1; :: thesis: verum

end;

hence p in Cl A by A4, Th15; :: thesis: verum

end;

now :: thesis: ( p in Cl A implies p in meet F )

assume A5: p in Cl A ; :: thesis: p in meet F

now :: thesis: for C being set st C in F holds
p in C

let C be set ; :: thesis: ( C in F implies p in C )
assume C in F ; :: thesis: p in C
then ex C1 being Subset of GX st
( C1 = C & C1 is closed & A c= C ) by A1;
hence p in C by A5, Th15; :: thesis: verum

end;

hence p in meet F by A2, SETFAM_1:def 1; :: thesis: verum

end;

hence ( p in Cl A iff p in meet F ) by A3; :: thesis: verum

end;

hence Cl A = meet F by TARSKI:2; :: thesis: verum