let T be non empty TA-structure ; :: thesis: for a being adjective of T holds types a = { t where t is type of T : a in adjs t }
let a be adjective of T; :: thesis: types a = { t where t is type of T : a in adjs t }
set X = { t where t is type of T : a in adjs t } ;
{ t where t is type of T : a in adjs t } c= the carrier of T

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { t where t is type of T : a in adjs t } or x in the carrier of T )
assume x in { t where t is type of T : a in adjs t } ; :: thesis: x in the carrier of T
then ex t being type of T st
( x = t & a in adjs t ) ;
hence x in the carrier of T ; :: thesis: verum

end;

then reconsider X = { t where t is type of T : a in adjs t } as Subset of T ;
for x being object holds
( x in X iff ex t being type of T st
( x = t & a in adjs t ) ) ;
hence types a = { t where t is type of T : a in adjs t } by Def12; :: thesis: verum