let D1, D2 be set ; :: thesis: ( ( for x being set holds
( x in D1 iff x is tagged_division of A ) ) & ( for x being set holds
( x in D2 iff x is tagged_division of A ) ) implies D1 = D2 )
assume that
A3: for x being set holds
( x in D1 iff x is tagged_division of A ) and
A4: for x being set holds
( x in D2 iff x is tagged_division of A ) ; :: thesis: D1 = D2
for x being object holds
( x in D1 iff x in D2 ) by A3, A4;
hence D1 = D2 by TARSKI:2; :: thesis: verum