let T be reflexive transitive antisymmetric with_suprema adj-structured TA-structure ; :: thesis: for a being adjective of T
for t being type of T st a is_applicable_to t holds
(types a) /\ (downarrow t) is Ideal of T
let a be adjective of T; :: thesis: for t being type of T st a is_applicable_to t holds
(types a) /\ (downarrow t) is Ideal of T
let t be type of T; :: thesis: ( a is_applicable_to t implies (types a) /\ (downarrow t) is Ideal of T )
given t9 being type of T such that A1: t9 in types a and
A2: t9 <= t ; :: according to ABCMIZ_0:def 15 :: thesis: (types a) /\ (downarrow t) is Ideal of T
t9 in downarrow t by A2, WAYBEL_0:17;
hence (types a) /\ (downarrow t) is Ideal of T by A1, WAYBEL_0:27, WAYBEL_0:44, XBOOLE_0:def 4; :: thesis: verum