let X be set ; :: thesis: for R being Relation

for Y being Subset of X st R is_asymmetric_in X holds

R is_asymmetric_in Y

let R be Relation; :: thesis: for Y being Subset of X st R is_asymmetric_in X holds

R is_asymmetric_in Y

let Y be Subset of X; :: thesis: ( R is_asymmetric_in X implies R is_asymmetric_in Y )

assume A1: R is_asymmetric_in X ; :: thesis: R is_asymmetric_in Y

for x, y being object st x in Y & y in Y & [x,y] in R holds

not [y,x] in R by A1, RELAT_2:def 5;

hence R is_asymmetric_in Y by RELAT_2:def 5; :: thesis: verum

for Y being Subset of X st R is_asymmetric_in X holds

R is_asymmetric_in Y

let R be Relation; :: thesis: for Y being Subset of X st R is_asymmetric_in X holds

R is_asymmetric_in Y

let Y be Subset of X; :: thesis: ( R is_asymmetric_in X implies R is_asymmetric_in Y )

assume A1: R is_asymmetric_in X ; :: thesis: R is_asymmetric_in Y

for x, y being object st x in Y & y in Y & [x,y] in R holds

not [y,x] in R by A1, RELAT_2:def 5;

hence R is_asymmetric_in Y by RELAT_2:def 5; :: thesis: verum