deffunc H₁( object ) -> Subset of S = SigFoaxTau (g,f,(CastBool ($1,S)),R,BASSIGN);
A1: for H being object st H in bool S holds
H₁(H) in bool S ;
consider IT being Function of (bool S),(bool S) such that
A2: for H being object st H in bool S holds
IT . H = H₁(H) from FUNCT_2:sch 2(A1);
A3: for H being Subset of S holds IT . H = SigFoaxTau (g,f,H,R,BASSIGN)

proof

let H be Subset of S; :: thesis: IT . H = SigFoaxTau (g,f,H,R,BASSIGN)
CastBool (H,S) = H by Def5;
hence IT . H = SigFoaxTau (g,f,H,R,BASSIGN) by A2; :: thesis: verum

end;

for H1, H2 being Subset of S st H1 c= H2 holds
IT . H1 c= IT . H2

proof

let H1, H2 be Subset of S; :: thesis: ( H1 c= H2 implies IT . H1 c= IT . H2 )
assume A4: H1 c= H2 ; :: thesis: IT . H1 c= IT . H2
A5: IT . H2 = SigFoaxTau (g,f,H2,R,BASSIGN) by A3;
IT . H1 = SigFoaxTau (g,f,H1,R,BASSIGN) by A3;
hence IT . H1 c= IT . H2 by A4, A5, Th45; :: thesis: verum

end;

then reconsider IT = IT as c=-monotone Function of (bool S),(bool S) by KNASTER:def 1;
take IT ; :: thesis: for H being Subset of S holds IT . H = SigFoaxTau (g,f,H,R,BASSIGN)
thus for H being Subset of S holds IT . H = SigFoaxTau (g,f,H,R,BASSIGN) by A3; :: thesis: verum