let Y be set ; :: thesis: for R being Relation st R is antisymmetric holds
R |_2 Y is antisymmetric
let R be Relation; :: thesis: ( R is antisymmetric implies R |_2 Y is antisymmetric )
assume A1: R is antisymmetric ; :: thesis: R |_2 Y is antisymmetric

now :: thesis: for a, b being object st [a,b] in R |_2 Y & [b,a] in R |_2 Y holds
a = b

let a, b be object ; :: thesis: ( [a,b] in R |_2 Y & [b,a] in R |_2 Y implies a = b )
assume ( [a,b] in R |_2 Y & [b,a] in R |_2 Y ) ; :: thesis: a = b
then ( [a,b] in R & [b,a] in R ) by XBOOLE_0:def 4;
hence a = b by A1, Lm3; :: thesis: verum

end;

hence R |_2 Y is antisymmetric by Lm3; :: thesis: verum