let T be with_closure with_properly_defined_topology 1TopStruct ; :: thesis: for A being Subset of T holds the FirstOp of T . A = Cl A
let A be Subset of T; :: thesis: the FirstOp of T . A = Cl A
set f = the FirstOp of T;
consider F being Subset-Family of T such that
A2: ( ( for C being Subset of T holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F ) by PRE_TOPC:16;
B1: the FirstOp of T is closure by CDef;
Z1: Cl A c= the FirstOp of T . A

proof

the FirstOp of T is idempotent by B1;
then the FirstOp of T . A is op-closed ;
then A3: the FirstOp of T . A is closed by Lem1;
the FirstOp of T is extensive by B1;
then the FirstOp of T . A in F by A3, A2;
hence Cl A c= the FirstOp of T . A by A2, SETFAM_1:3; :: thesis: verum

end;

the FirstOp of T is closure by CDef;
then N2: the FirstOp of T is c=-monotone ;
defpred S₁[ Subset of T] means $1 in F;
set G = { ( the FirstOp of T . B) where B is Subset of T : B in F } ;
deffunc H₁() -> Element of bool (bool the carrier of T) = bool the carrier of T;
deffunc H₂( Element of H₁()) -> Element of bool the carrier of T = the FirstOp of T . $1;
deffunc H₃( Element of H₁()) -> Element of H₁() = $1;
TT: for B being Element of H₁() st S₁[B] holds
H₂(B) = H₃(B)

proof

let B be Subset of T; :: thesis: ( S₁[B] implies H₂(B) = H₃(B) )
assume B in F ; :: thesis: H₂(B) = H₃(B)
then B is op-closed by Lem1, A2;
hence H₂(B) = H₃(B) ; :: thesis: verum

end;

{ H₂(B) where B is Element of H₁() : S₁[B] } = { H₃(B) where B is Element of H₁() : S₁[B] } from FRAENKEL:sch 6(TT);
then f3: F = { ( the FirstOp of T . B) where B is Subset of T : B in F } by Lemma;
( [#] T is closed & A c= [#] T ) ;
then j1: { ( the FirstOp of T . B) where B is Subset of T : B in F } <> {} by f3, A2;
for Z1 being set st Z1 in { ( the FirstOp of T . B) where B is Subset of T : B in F } holds
the FirstOp of T . A c= Z1

proof

let Z1 be set ; :: thesis: ( Z1 in { ( the FirstOp of T . B) where B is Subset of T : B in F } implies the FirstOp of T . A c= Z1 )
assume Z1 in { ( the FirstOp of T . B) where B is Subset of T : B in F } ; :: thesis: the FirstOp of T . A c= Z1
then ex B being Subset of T st
( Z1 = the FirstOp of T . B & B in F ) ;
hence the FirstOp of T . A c= Z1 by N2, A2; :: thesis: verum

end;

hence the FirstOp of T . A = Cl A by Z1, A2, f3, j1, SETFAM_1:5; :: thesis: verum