let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; 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; 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; ( 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
; ( 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; ( 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
a ast (b ast t) = b ast (a ast t)
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))
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; verum