let X be set ; :: thesis:
let f be c=-monotone Function of (bool X),(bool X); :: thesis:
defpred S₁[ set ] means f . $1 c= $1;
reconsider H = { h where h is Subset of X : S₁[h] } as Subset-Family of X from DOMAIN_1:sch 7();
reconsider H = H as Subset-Family of X ;
set A = meet H;

X c= X ;
then reconsider X9 = X as Subset of X ;
f . X9 c= X9 ;
then X9 in H ;
hence H <> {} ; :: thesis:
let h be set ; :: thesis:
assume A1: h in H ; :: thesis:
then consider x being Subset of X such that
A2: x = h and
A3: f . x c= x ;
meet H c= h by A1, SETFAM_1:3;
then f . (meet H) c= f . x by A2, Def1;
hence f . (meet H) c= h by A2, A3; :: thesis:

end;