let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; :: thesis: T @--> is irreflexive
set R = T @--> ;
let x be set ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: ( not x in field (T @--> ) or not [x,x] in T @--> )
assume x in field (T @--> ) ; :: thesis: not [x,x] in T @-->
assume A1: [x,x] in T @--> ; :: thesis: contradiction
then reconsider x = x as type of T by ZFMISC_1:106;
consider a being adjective of T such that
A2: not a in adjs x and
A3: a is_properly_applicable_to x and
A4: a ast x = x by A1, Def31;
a is_applicable_to x by A3, Def27;
hence contradiction by A2, A4, Th22; :: thesis: verum