let R be Relation; :: thesis: for X being set st R is_antisymmetric_in X holds
R |_2 X is antisymmetric
let X be set ; :: thesis: ( R is_antisymmetric_in X implies R |_2 X is antisymmetric )
assume A1: for x, y being set st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y ; :: according to RELAT_2:def 4 :: thesis: R |_2 X is antisymmetric
let x be set ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: for b₁ being set holds
( not x in field (R |_2 X) or not b₁ in field (R |_2 X) or not [x,b₁] in R |_2 X or not [b₁,x] in R |_2 X or x = b₁ )
let y be set ; :: thesis: ( not x in field (R |_2 X) or not y in field (R |_2 X) or not [x,y] in R |_2 X or not [y,x] in R |_2 X or x = y )
assume ( x in field (R |_2 X) & y in field (R |_2 X) ) ; :: thesis: ( not [x,y] in R |_2 X or not [y,x] in R |_2 X or x = y )
then A2: ( x in X & y in X ) by WELLORD1:19;
assume ( [x,y] in R |_2 X & [y,x] in R |_2 X ) ; :: thesis: x = y
then ( [x,y] in R & [y,x] in R ) by XBOOLE_0:def 4;
hence x = y by A1, A2; :: thesis: verum