deffunc H₁( Subset of (Funcs (Q,Q))) -> Subset of (Funcs (Q,Q)) = MltClos1 (H,$1);
consider phi being Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) such that
A1: for X being Subset of (Funcs (Q,Q)) holds phi . X = H₁(X) from FUNCT_2:sch 4();
reconsider phi = phi as c=-monotone Function of (bool (Funcs (Q,Q))),(bool (Funcs (Q,Q))) by A1, Th26;
set Y = lfp ((Funcs (Q,Q)),phi);
A2: lfp ((Funcs (Q,Q)),phi) is_a_fixpoint_of phi by KNASTER:4;
then A3: ( lfp ((Funcs (Q,Q)),phi) in dom phi & lfp ((Funcs (Q,Q)),phi) = phi . (lfp ((Funcs (Q,Q)),phi)) & phi . (lfp ((Funcs (Q,Q)),phi)) = H₁( lfp ((Funcs (Q,Q)),phi)) ) by ABIAN:def 3, A1;
A4: for S being Subset of (Funcs (Q,Q)) st phi . S c= S holds
lfp ((Funcs (Q,Q)),phi) c= S by KNASTER:6;
reconsider Y = lfp ((Funcs (Q,Q)),phi) as composition-closed inverse-closed Subset of (Funcs (Q,Q)) by Th29, A1, A2, A4;
take Y ; :: thesis: ( H left-right-mult-closed Y & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds
Y c= X ) )
thus H left-right-mult-closed Y by Th27, A1, A3; :: thesis: for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds
Y c= X
let S be composition-closed inverse-closed Subset of (Funcs (Q,Q)); :: thesis: ( H left-right-mult-closed S implies Y c= S )
assume A5: H left-right-mult-closed S ; :: thesis: Y c= S
phi . S c= S

proof

let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in phi . S or f in S )
assume f in phi . S ; :: thesis: f in S
then f in H₁(S) by A1;
then S₂[Q,H,S,f] by Def37;
hence f in S by A5, Def34, Def35; :: thesis: verum

end;

hence Y c= S by KNASTER:6; :: thesis: verum