let x be object ; :: thesis: for R being Relation st R is irreflexive holds
not [x,x] in R
let R be Relation; :: thesis: ( R is irreflexive implies not [x,x] in R )
assume A1: R is irreflexive ; :: thesis: not [x,x] in R
assume A2: [x,x] in R ; :: thesis: contradiction
then x in field R by RELAT_1:15;
hence contradiction by A1, RELAT_2:def 10, A2, RELAT_2:def 2; :: thesis: verum