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 S1[ Subset of T] means $1 in F;
set G = { ( the FirstOp of T . B) where B is Subset of T : B in F } ;
deffunc H1() -> Element of bool (bool the carrier of T) = bool the carrier of T;
deffunc H2( Element of H1()) -> Element of bool the carrier of T = the FirstOp of T . $1;
deffunc H3( Element of H1()) -> Element of H1() = $1;
TT: for B being Element of H1() st S1[B] holds
H2(B) = H3(B)
proof
let B be Subset of T; :: thesis: ( S1[B] implies H2(B) = H3(B) )
assume B in F ; :: thesis: H2(B) = H3(B)
then B is op-closed by Lem1, A2;
hence H2(B) = H3(B) ; :: thesis: verum
end;
{ H2(B) where B is Element of H1() : S1[B] } = { H3(B) where B is Element of H1() : S1[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