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

R \/ (id X) is_antisymmetric_in X

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

assume A1: R is_asymmetric_in X ; :: thesis: R \/ (id X) is_antisymmetric_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 \/ (id X) & [y,x] in R \/ (id X) holds

x = y

let y be object ; :: thesis: ( x in X & y in X & [x,y] in R \/ (id X) & [y,x] in R \/ (id X) implies x = y )

assume that

A2: ( x in X & y in X ) and

A3: [x,y] in R \/ (id X) and

A4: [y,x] in R \/ (id X) ; :: thesis: x = y

assume A5: x <> y ; :: thesis: contradiction

then not [y,x] in id X by RELAT_1:def 10;

then A6: [y,x] in R by A4, XBOOLE_0:def 3;

not [x,y] in id X by A5, RELAT_1:def 10;

then [x,y] in R by A3, XBOOLE_0:def 3;

hence contradiction by A1, A2, A6; :: thesis: verum

R \/ (id X) is_antisymmetric_in X

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

assume A1: R is_asymmetric_in X ; :: thesis: R \/ (id X) is_antisymmetric_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 \/ (id X) & [y,x] in R \/ (id X) holds

x = y

let y be object ; :: thesis: ( x in X & y in X & [x,y] in R \/ (id X) & [y,x] in R \/ (id X) implies x = y )

assume that

A2: ( x in X & y in X ) and

A3: [x,y] in R \/ (id X) and

A4: [y,x] in R \/ (id X) ; :: thesis: x = y

assume A5: x <> y ; :: thesis: contradiction

then not [y,x] in id X by RELAT_1:def 10;

then A6: [y,x] in R by A4, XBOOLE_0:def 3;

not [x,y] in id X by A5, RELAT_1:def 10;

then [x,y] in R by A3, XBOOLE_0:def 3;

hence contradiction by A1, A2, A6; :: thesis: verum