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

for Y being Subset of X st R is_symmetric_in X holds

R is_symmetric_in Y

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

R is_symmetric_in Y

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

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

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

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

hence R is_symmetric_in Y by RELAT_2:def 3; :: thesis: verum

for Y being Subset of X st R is_symmetric_in X holds

R is_symmetric_in Y

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

R is_symmetric_in Y

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

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

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

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

hence R is_symmetric_in Y by RELAT_2:def 3; :: thesis: verum