let T be TA-structure ; :: thesis: for t being type of T
for A, B being Subset of 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 st A is_applicable_to t & B c= A holds
B is_applicable_to t
let A, B be Subset of ; :: thesis: ( A is_applicable_to t & B c= A implies B is_applicable_to t )
given t' being type of T such that A1: A c= adjs t' and
A2: t' <= 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 t' ; :: according to ABCMIZ_0:def 16 :: thesis: ( B c= adjs t' & t' <= t )
thus ( B c= adjs t' & t' <= t ) by A1, A2, A3, XBOOLE_1:1; :: thesis: verum