let T be TA-structure ; :: thesis: for t being type of T
for A, B being Subset of the adjectives of T st A is_applicable_to t & B c= A holds
B is_applicable_to t
let t be type of T; :: thesis: for A, B being Subset of the adjectives of T st A is_applicable_to t & B c= A holds
B is_applicable_to t
let A, B be Subset of the adjectives of T; :: thesis: ( A is_applicable_to t & B c= A implies B is_applicable_to t )
given t9 being type of T such that A1: A c= adjs t9 and
A2: t9 <= t ; :: according to ABCMIZ_0:def 16 :: thesis: ( not B c= A or B is_applicable_to t )
assume A3: B c= A ; :: thesis: B is_applicable_to t
take t9 ; :: according to ABCMIZ_0:def 16 :: thesis: ( B c= adjs t9 & t9 <= t )
thus ( B c= adjs t9 & t9 <= t ) by A1, A2, A3; :: thesis: verum