let D1, D2 be non empty Subset-Family of X; :: thesis: ( ( for A being Subset of X holds
( A in D1 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ) & ( for A being Subset of X holds
( A in D2 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ) implies D1 = D2 )
assume that
A4: for A being Subset of X holds
( A in D1 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) and
A5: for A being Subset of X holds
( A in D2 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ; :: thesis: D1 = D2
for A being set holds
( A in D1 iff A in D2 )

proof

let A be set ; :: thesis: ( A in D1 iff A in D2 )

hereby :: thesis: ( A in D2 implies A in D1 )

assume A6: A in D1 ; :: thesis: A in D2
then reconsider A' = A as Subset of 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 A4, A6;
hence A in D2 by A5; :: thesis: verum

end;

assume A7: A in D2 ; :: thesis: A in D1
then reconsider A = A as Subset of 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 A5, A7;
hence A in D1 by A4; :: thesis: verum

end;

hence D1 = D2 by TARSKI:2; :: thesis: verum