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