let T be non empty TA-structure ; :: thesis: for t being type of T
for A being Subset of the adjectives of T holds
( A c= adjs t iff t in types A )
let t be type of T; :: thesis: for A being Subset of the adjectives of T holds
( A c= adjs t iff t in types A )
let a be Subset of the adjectives of T; :: thesis: ( a c= adjs t iff t in types a )

hereby :: thesis: ( t in types a implies a c= adjs t )

assume a c= adjs t ; :: thesis: t in types a
then for b being adjective of T st b in a holds
t in types b by Th13;
hence t in types a by Def13; :: thesis: verum

end;

assume A1: t in types a ; :: thesis: a c= adjs t
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a or x in adjs t )
assume A2: x in a ; :: thesis: x in adjs t
then reconsider x = x as adjective of T ;
t in types x by A1, A2, Def13;
hence x in adjs t by Th13; :: thesis: verum