let T be non empty reflexive transitive non void TAS-structure ; :: thesis: for t being type of T holds {} the adjectives of T is_properly_applicable_to t
let t be type of T; :: thesis: {} the adjectives of T is_properly_applicable_to t
take s = <*> the adjectives of T; :: according to ABCMIZ_0:def 29 :: thesis: ( rng s = {} the adjectives of T & s is_properly_applicable_to t )
thus rng s = {} the adjectives of T ; :: thesis: s is_properly_applicable_to t
let i be Nat; :: according to ABCMIZ_0:def 28 :: thesis: for a being adjective of T
for s being type of T st i in dom s & a = s . i & s = (apply (s,t)) . i holds
a is_properly_applicable_to s
thus for a being adjective of T
for s being type of T st i in dom s & a = s . i & s = (apply (s,t)) . i holds
a is_properly_applicable_to s ; :: thesis: verum