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) )
consider t9 being type of T such that
A3: t9 in types b and
A4: t9 <= a ast t by A2;
A5: b in adjs t9 by A3, Th13;
A6: a ast t <= t by A1, Th20;
thus A7: b is_applicable_to t by A6, A3, A4, YELLOW_0:def 2; :: thesis: ( a is_applicable_to b ast t & a ast (b ast t) = b ast (a ast t) )
A8: t9 <= t by A6, A4, YELLOW_0:def 2;
thus A9: a is_applicable_to b ast t :: thesis: a ast (b ast t) = b ast (a ast t)

proof

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

end;

then A10: a ast (b ast t) <= b ast t by Th20;
A11: a ast t in types a by A1, Th22;
A12: a ast (b ast t) is_>=_than (types b) /\ (downarrow (a ast t))

proof

let t9 be type of T; :: according to LATTICE3:def 9 :: thesis: ( not t9 in (types b) /\ (downarrow (a ast t)) or t9 <= a ast (b ast t) )
assume A13: t9 in (types b) /\ (downarrow (a ast t)) ; :: thesis: t9 <= a ast (b ast t)
then t9 in types b by XBOOLE_0:def 4;
then A14: b in adjs t9 by Th13;
t9 in downarrow (a ast t) by A13, XBOOLE_0:def 4;
then A15: t9 <= a ast t by WAYBEL_0:17;
then t9 in types a by A11, WAYBEL_0:def 19;
then A16: a in adjs t9 by Th13;
t9 <= t by A6, A15, YELLOW_0:def 2;
then t9 <= b ast t by A14, Th23;
hence t9 <= a ast (b ast t) by A16, Th23; :: thesis: verum

end;

b ast t <= t by A7, Th20;
then A17: a ast (b ast t) <= t by A10, YELLOW_0:def 2;
a in adjs (a ast (b ast t)) by A9, Th21;
then a ast (b ast t) <= a ast t by A17, Th23;
then A18: a ast (b ast t) in downarrow (a ast t) by WAYBEL_0:17;
A19: a ast (b ast t) <= b ast t by A9, Th20;
b ast t in types b by A7, Th22;
then a ast (b ast t) in types b by A19, WAYBEL_0:def 19;
then a ast (b ast t) in (types b) /\ (downarrow (a ast t)) by A18, XBOOLE_0:def 4;
then for t9 being type of T st t9 is_>=_than (types b) /\ (downarrow (a ast t)) holds
a ast (b ast t) <= t9 ;
hence a ast (b ast t) = b ast (a ast t) by A12, YELLOW_0:30; :: thesis: verum