let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; :: thesis: for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
A is_applicable_to t
let t be type of T; :: thesis: for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
A is_applicable_to t
let v be FinSequence of the adjectives of T; :: thesis: ( v is_applicable_to t implies for A being Subset of the adjectives of T st A = rng v holds
A is_applicable_to t )
assume v is_applicable_to t ; :: thesis: for A being Subset of the adjectives of T st A = rng v holds
A is_applicable_to t
then ( v ast t <= t & rng v c= adjs (v ast t) ) by Th44, Th45;
hence for A being Subset of the adjectives of T st A = rng v holds
A is_applicable_to t by Def16; :: thesis: verum