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
A6: 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
A7: 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 object holds
( A in D1 iff A in D2 )

proof

let A be object ; :: thesis: ( A in D1 iff A in D2 )
reconsider AA = A as set by TARSKI:1;

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

assume A8: A in D1 ; :: thesis: A in D2
then reconsider A9 = A as Subset of X ;
for W, Z being Subset of X st W c= AA & Z c= X \ A9 holds
(C . W) + (C . Z) <= C . (W \/ Z) by A6, A8;
hence A in D2 by A7; :: thesis: verum

end;

assume A9: 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 A7, A9;
hence A in D1 by A6; :: thesis: verum

end;

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