reconsider A = {} as Subset of X by XBOOLE_1:2;
defpred S₁[ set ] means for A being set st A = $1 holds
for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z);
consider D being set such that
A1: for y being set holds
( y in D iff ( y in bool X & S₁[y] ) ) from XFAMILY:sch 1();
A2: for A being set holds
( A in D iff ( A in bool X & ( for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ) )

proof

let A be set ; :: thesis: ( A in D iff ( A in bool X & ( for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ) )
( S₁[A] iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ;
hence ( A in D iff ( A in bool X & ( for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ) ) by A1; :: thesis: verum

end;

then A3: for A being object st A in D holds
A in bool X ;

now :: thesis: for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z)

let W, Z be Subset of X; :: thesis: ( W c= A & Z c= X \ A implies (C . W) + (C . Z) <= C . (W \/ Z) )
assume that
A4: W c= A and
Z c= X \ A ; :: thesis: (C . W) + (C . Z) <= C . (W \/ Z)
A5: W = {} by A4;
C is zeroed by Def1;
then C . W = 0 by A5, VALUED_0:def 19;
hence (C . W) + (C . Z) <= C . (W \/ Z) by A5, XXREAL_3:4; :: thesis: verum

end;

then reconsider D = D as non empty Subset-Family of X by A2, A3, TARSKI:def 3;
take D ; :: thesis: for A being Subset of X holds
( A in D iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) )
thus for A being Subset of X holds
( A in D iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) by A2; :: thesis: verum