let X be set ; :: thesis: for R being Relation holds

( R is_antisymmetric_in X iff R \ (id X) is_asymmetric_in X )

let R be Relation; :: thesis: ( R is_antisymmetric_in X iff R \ (id X) is_asymmetric_in X )

let x be object ; :: according to RELAT_2:def 4 :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: x = y

assume A10: x <> y ; :: thesis: 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; :: thesis: verum

( R is_antisymmetric_in X iff R \ (id X) is_asymmetric_in X )

let R be Relation; :: thesis: ( R is_antisymmetric_in X iff R \ (id X) is_asymmetric_in X )

hereby :: thesis: ( R \ (id X) is_asymmetric_in X implies R is_antisymmetric_in X )

assume A6:
R \ (id X) is_asymmetric_in X
; :: thesis: R is_antisymmetric_in Xassume A1:
R is_antisymmetric_in X
; :: thesis: R \ (id X) is_asymmetric_in X

thus R \ (id X) is_asymmetric_in X :: thesis: verum

end;thus R \ (id X) is_asymmetric_in X :: thesis: verum

proof

let x be object ; :: according to RELAT_2:def 5 :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum

end;not [y,x] in R \ (id X)

let y be object ; :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum

let x be object ; :: according to RELAT_2:def 4 :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: x = y

assume A10: x <> y ; :: thesis: 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; :: thesis: verum