let T be TA-structure ; :: thesis: for t being type of T
for a being adjective of T holds
( a in adjs t iff t in types a )
let t be type of T; :: thesis: for a being adjective of T holds
( a in adjs t iff t in types a )
let a be adjective of T; :: thesis: ( a in adjs t iff t in types a )
thus ( a in adjs t implies t in types a ) by Def12; :: thesis: ( t in types a implies a in adjs t )
assume t in types a ; :: thesis: a in adjs t
then ex t9 being type of T st
( t = t9 & a in adjs t9 ) by Def12;
hence a in adjs t ; :: thesis: verum