let T be non void TA-structure ; :: thesis: for t being type of T holds adjs t = { a where a is adjective of T : t in types a }
let t be type of T; :: thesis: adjs t = { a where a is adjective of T : t in types a }
set X = { a where a is adjective of T : t in types a } ;
thus adjs t c= { a where a is adjective of T : t in types a } :: according to XBOOLE_0:def 10 :: thesis: { a where a is adjective of T : t in types a } c= adjs t

proof

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

end;

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