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 object ; :: 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:87;
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;
hence contradiction by A2, A4, Th21; :: thesis: verum