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 object 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, y be object ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: 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 that
A2: x in field (R |_2 X) and
A3: 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 )
A4: y in X by A3, WELLORD1:12;
assume that
A5: [x,y] in R |_2 X and
A6: [y,x] in R |_2 X ; :: thesis: x = y
A7: [x,y] in R by A5, XBOOLE_0:def 4;
A8: [y,x] in R by A6, XBOOLE_0:def 4;
x in X by A2, WELLORD1:12;
hence x = y by A1, A4, A7, A8; :: thesis: verum