let T be reflexive transitive antisymmetric with_suprema TA-structure ; :: thesis: ( T is adj-structured implies for t1, t2 being type of T st t1 <= t2 holds
adjs t2 c= adjs t1 )
assume A1: for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) ; :: according to ABCMIZ_0:def 11 :: thesis: for t1, t2 being type of T st t1 <= t2 holds
adjs t2 c= adjs t1
let t1, t2 be type of T; :: thesis: ( t1 <= t2 implies adjs t2 c= adjs t1 )
assume t1 <= t2 ; :: thesis: adjs t2 c= adjs t1
then t1 "\/" t2 = t2 by YELLOW_0:24;
then adjs t2 = (adjs t1) /\ (adjs t2) by A1;
hence adjs t2 c= adjs t1 by XBOOLE_1:17; :: thesis: verum