let T be reflexive transitive antisymmetric with_suprema adj-structured TA-structure ; :: thesis: for A being Subset of
for t being type of T st A is_applicable_to t holds
(types A) /\ (downarrow t) is Ideal of T
let A be Subset of ; :: 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 t' being type of T such that A1: A c= adjs t' and
A2: t' <= t ; :: according to ABCMIZ_0:def 16 :: thesis: (types A) /\ (downarrow t) is Ideal of T
A3: t' in downarrow t by A2, WAYBEL_0:17;
t' in types A by A1, Th14;
hence (types A) /\ (downarrow t) is Ideal of T by A3, WAYBEL_0:27, WAYBEL_0:44, XBOOLE_0:def 4; :: thesis: verum