let X1, X2 be Subset of T; :: thesis: ( ( for t being type of T holds
( t in X1 iff for a being adjective of T st a in A holds
t in types a ) ) & ( for t being type of T holds
( t in X2 iff for a being adjective of T st a in A holds
t in types a ) ) implies X1 = X2 )
assume that
A2: for t being type of T holds
( t in X1 iff for a being adjective of T st a in A holds
t in types a ) and
A3: for t being type of T holds
( t in X2 iff for a being adjective of T st a in A holds
t in types a ) ; :: thesis: X1 = X2

now :: thesis: for x being object holds
( x in X1 iff x in X2 )

let x be object ; :: thesis: ( x in X1 iff x in X2 )
( x in X1 iff ( x is type of T & ( for a being adjective of T st a in A holds
x in types a ) ) ) by A2;
hence ( x in X1 iff x in X2 ) by A3; :: thesis: verum

end;

hence X1 = X2 by TARSKI:2; :: thesis: verum