let D1, D2 be set ; :: thesis: ( ( for x1 being set holds
( x1 in D1 iff x1 is Division of A ) ) & ( for x1 being set holds
( x1 in D2 iff x1 is Division of A ) ) implies D1 = D2 )
assume that
A2: for x1 being set holds
( x1 in D1 iff x1 is Division of A ) and
A3: for x1 being set holds
( x1 in D2 iff x1 is Division of A ) ; :: thesis: D1 = D2

now :: thesis: for x1 being object holds
( ( x1 in D1 implies x1 in D2 ) & ( x1 in D2 implies x1 in D1 ) )

let x1 be object ; :: thesis: ( ( x1 in D1 implies x1 in D2 ) & ( x1 in D2 implies x1 in D1 ) )
thus ( x1 in D1 implies x1 in D2 ) :: thesis: ( x1 in D2 implies x1 in D1 )

proof

assume x1 in D1 ; :: thesis: x1 in D2
then x1 is Division of A by A2;
hence x1 in D2 by A3; :: thesis: verum

end;

assume x1 in D2 ; :: thesis: x1 in D1
then x1 is Division of A by A3;
hence x1 in D1 by A2; :: thesis: verum

end;

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