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

proof

let G be Subset of S; :: thesis: IT . G = SigFaxTau (f,G,R,BASSIGN)
H₁(G) = SigFaxTau (f,G,R,BASSIGN) by Def5;
hence IT . G = SigFaxTau (f,G,R,BASSIGN) by A2; :: thesis: verum

end;

for G1, G2 being Subset of S st G1 c= G2 holds
IT . G1 c= IT . G2

proof

let G1, G2 be Subset of S; :: thesis: ( G1 c= G2 implies IT . G1 c= IT . G2 )
assume A4: G1 c= G2 ; :: thesis: IT . G1 c= IT . G2
A5: IT . G2 = SigFaxTau (f,G2,R,BASSIGN) by A3;
IT . G1 = SigFaxTau (f,G1,R,BASSIGN) by A3;
hence IT . G1 c= IT . G2 by A4, A5, Th37; :: thesis: verum

end;

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