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

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

hence
R |_2 Y is antisymmetric
by Lm3; :: thesis: veruma = 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;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