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

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