let T be non empty TA-structure ; :: thesis: types ({} the adjectives of T) = the carrier of T
thus types ({} the adjectives of T) c= the carrier of T ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of T c= types ({} the adjectives of T)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of T or x in types ({} the adjectives of T) )
assume x in the carrier of T ; :: thesis: x in types ({} the adjectives of T)
then reconsider t = x as type of T ;
for a being adjective of T st a in {} the adjectives of T holds
t in types a ;
hence x in types ({} the adjectives of T) by Def13; :: thesis: verum