let T be non empty reflexive transitive non void TAS-structure ; :: thesis: for t being type of T
for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
A is finite
let t be type of T; :: thesis: for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
A is finite
let A be Subset of the adjectives of T; :: thesis: ( A is_properly_applicable_to t implies A is finite )
assume ex s being FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t ) ; :: according to ABCMIZ_0:def 29 :: thesis: A is finite
hence A is finite ; :: thesis: verum