let X be set ; for R being Relation holds
( R is_antisymmetric_in X iff R \ (id X) is_asymmetric_in X )
let R be Relation; ( R is_antisymmetric_in X iff R \ (id X) is_asymmetric_in X )
hereby ( R \ (id X) is_asymmetric_in X implies R is_antisymmetric_in X )
assume A1:
R is_antisymmetric_in X
;
R \ (id X) is_asymmetric_in Xthus
R \ (id X) is_asymmetric_in X
verumproof
let x be
object ;
RELAT_2:def 5 for y being object st x in X & y in X & [x,y] in R \ (id X) holds
not [y,x] in R \ (id X)let y be
object ;
( x in X & y in X & [x,y] in R \ (id X) implies not [y,x] in R \ (id X) )
assume that A2:
x in X
and A3:
y in X
and A4:
[x,y] in R \ (id X)
;
not [y,x] in R \ (id X)
not
[x,y] in id X
by A4, XBOOLE_0:def 5;
then A5:
x <> y
by A2, RELAT_1:def 10;
[x,y] in R
by A4, XBOOLE_0:def 5;
then
not
[y,x] in R
by A1, A2, A3, A5;
hence
not
[y,x] in R \ (id X)
by XBOOLE_0:def 5;
verum
end;
end;
assume A6:
R \ (id X) is_asymmetric_in X
; R is_antisymmetric_in X
let x be object ; RELAT_2:def 4 for y being object st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y
let y be object ; ( x in X & y in X & [x,y] in R & [y,x] in R implies x = y )
assume that
A7:
( x in X & y in X )
and
A8:
[x,y] in R
and
A9:
[y,x] in R
; x = y
assume A10:
x <> y
; contradiction
then
not [y,x] in id X
by RELAT_1:def 10;
then A11:
[y,x] in R \ (id X)
by A9, XBOOLE_0:def 5;
not [x,y] in id X
by A10, RELAT_1:def 10;
then
[x,y] in R \ (id X)
by A8, XBOOLE_0:def 5;
hence
contradiction
by A6, A7, A11; verum