let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; :: thesis: for t being type of T
for a, b being adjective of T st a is_applicable_to t & b is_applicable_to a ast t holds
( b is_applicable_to t & a is_applicable_to b ast t & a ast (b ast t) = b ast (a ast t) )
let t be type of T; :: thesis: for a, b being adjective of T st a is_applicable_to t & b is_applicable_to a ast t holds
( b is_applicable_to t & a is_applicable_to b ast t & a ast (b ast t) = b ast (a ast t) )
let a, b be adjective of T; :: thesis: ( a is_applicable_to t & b is_applicable_to a ast t implies ( b is_applicable_to t & a is_applicable_to b ast t & a ast (b ast t) = b ast (a ast t) ) )
assume that
A1: a is_applicable_to t and
A2: b is_applicable_to a ast t ; :: thesis: ( b is_applicable_to t & a is_applicable_to b ast t & a ast (b ast t) = b ast (a ast t) )
A3: ( a ast t = sup ((types a) /\ (downarrow t)) & a ast t <= t & a ast t in types a ) by A1, Th21, Th23;
consider t' being type of T such that
A4: ( t' in types b & t' <= a ast t ) by A2, Def15;
A5: ( t' <= t & b in adjs t' ) by A3, A4, Th13, YELLOW_0:def 2;
thus b is_applicable_to t :: thesis: ( a is_applicable_to b ast t & a ast (b ast t) = b ast (a ast t) )

proof

take t' ; :: according to ABCMIZ_0:def 15 :: thesis: ( t' in types b & t' <= t )
thus ( t' in types b & t' <= t ) by A3, A4, YELLOW_0:def 2; :: thesis: verum

end;

then A6: ( b ast t = sup ((types b) /\ (downarrow t)) & b ast t <= t & b ast t in types b ) by Th21, Th23;
thus A7: a is_applicable_to b ast t :: thesis: a ast (b ast t) = b ast (a ast t)

proof

take t' ; :: according to ABCMIZ_0:def 15 :: thesis: ( t' in types a & t' <= b ast t )
a ast t in types a by A1, Th23;
hence t' in types a by A4, WAYBEL_0:def 19; :: thesis: t' <= b ast t
thus t' <= b ast t by A5, Th24; :: thesis: verum

end;

A8: a ast (b ast t) is_>=_than (types b) /\ (downarrow (a ast t))

proof

let t' be type of T; :: according to LATTICE3:def 9 :: thesis: ( not t' in (types b) /\ (downarrow (a ast t)) or t' <= a ast (b ast t) )
assume t' in (types b) /\ (downarrow (a ast t)) ; :: thesis: t' <= a ast (b ast t)
then ( t' in types b & t' in downarrow (a ast t) ) by XBOOLE_0:def 4;
then A9: ( b in adjs t' & t' <= a ast t ) by Th13, WAYBEL_0:17;
then ( t' <= t & t' in types a ) by A3, WAYBEL_0:def 19, YELLOW_0:def 2;
then ( t' <= b ast t & a in adjs t' ) by A9, Th13, Th24;
hence t' <= a ast (b ast t) by Th24; :: thesis: verum

end;

a ast (b ast t) <= b ast t by A7, Th21;
then ( a ast (b ast t) <= t & a in adjs (a ast (b ast t)) ) by A6, A7, Th22, YELLOW_0:def 2;
then ( a ast (b ast t) <= b ast t & a ast (b ast t) <= a ast t ) by A7, Th21, Th24;
then ( a ast (b ast t) in types b & a ast (b ast t) in downarrow (a ast t) ) by A6, WAYBEL_0:17, WAYBEL_0:def 19;
then a ast (b ast t) in (types b) /\ (downarrow (a ast t)) by XBOOLE_0:def 4;
then for t' being type of T st t' is_>=_than (types b) /\ (downarrow (a ast t)) holds
a ast (b ast t) <= t' by LATTICE3:def 9;
hence a ast (b ast t) = b ast (a ast t) by A8, YELLOW_0:30; :: thesis: verum