let X be set ; :: thesis: for R being Relation
for Y being Subset of X st R is_irreflexive_in X holds
R is_irreflexive_in Y
let R be Relation; :: thesis: for Y being Subset of X st R is_irreflexive_in X holds
R is_irreflexive_in Y
let Y be Subset of X; :: thesis: ( R is_irreflexive_in X implies R is_irreflexive_in Y )
assume A1: R is_irreflexive_in X ; :: thesis: R is_irreflexive_in Y
for x being object st x in Y holds
not [x,x] in R by A1, RELAT_2:def 2;
hence R is_irreflexive_in Y by RELAT_2:def 2; :: thesis: verum