let X, S be non empty set ; :: thesis: for R being Relation of X st R is antisymmetric & field R c= S holds
R is_antisymmetric_in S
let R be Relation of X; :: thesis: ( R is antisymmetric & field R c= S implies R is_antisymmetric_in S )
assume ( R is antisymmetric & field R c= S ) ; :: thesis: R is_antisymmetric_in S
then A1: R is_antisymmetric_in field R by RELAT_2:def 12;
let x, y be set ; :: according to RELAT_2:def 4 :: thesis: ( not x in S or not y in S or not [x,y] in R or not [y,x] in R or x = y )
assume ( x in S & y in S ) ; :: thesis: ( not [x,y] in R or not [y,x] in R or x = y )
assume A2: [x,y] in R ; :: thesis: ( not [y,x] in R or x = y )
assume A3: [y,x] in R ; :: thesis: x = y
( x in field R & y in field R ) by A2, RELAT_1:30;
hence x = y by A1, A2, A3, RELAT_2:def 4; :: thesis: verum