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 A1: 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 A2: rng v c= adjs (v ast t) by Th44;
v ast t <= t by A1, Th43;
hence for A being Subset of the adjectives of T st A = rng v holds
A is_applicable_to t by A2; :: thesis: verum