let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; :: thesis: T @--> c= the InternalRel of T
let t1, t2 be Element of T; :: according to RELSET_1:def 1 :: thesis: ( not [t1,t2] in T @--> or [t1,t2] in the InternalRel of T )
reconsider q1 = t1, q2 = t2 as type of T ;
assume [t1,t2] in T @--> ; :: thesis: [t1,t2] in the InternalRel of T
then consider a being adjective of T such that
not a in adjs q2 and
A1: a is_properly_applicable_to q2 and
A2: a ast q2 = q1 by Def31;
a is_applicable_to q2 by A1;
then q1 <= q2 by A2, Th20;
hence [t1,t2] in the InternalRel of T by ORDERS_2:def 5; :: thesis: verum