let X be non empty set ; :: thesis: for R being Relation of X st R is_irreflexive_in X holds
R is irreflexive
let R be Relation of X; :: thesis: ( R is_irreflexive_in X implies R is irreflexive )
A1: field R c= X \/ X by RELSET_1:8;
assume R is_irreflexive_in X ; :: thesis: R is irreflexive
then for x being object st x in field R holds
not [x,x] in R by A1;
then R is_irreflexive_in field R ;
hence R is irreflexive ; :: thesis: verum