reconsider A = {} as Subset of X byXBOOLE_1:2; defpred S1[ 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 inbool X & S1[y] ) )
fromXFAMILY:sch 1(); A2:
for A being set holds ( A in D iff ( A inbool X & ( for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W)+(C . Z)<= C .(W \/ Z) ) ) )
let A be set ; :: thesis: ( A in D iff ( A inbool X & ( for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W)+(C . Z)<= C .(W \/ Z) ) ) )
( S1[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 inbool X & ( for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W)+(C . Z)<= C .(W \/ Z) ) ) )
byA1; :: thesis: verum
end;
then A3:
for A being object st A in D holds A inbool X
;