let X be set ; :: thesis: for R being Relation st R = id X holds
( R is reflexive & R is symmetric & R is antisymmetric & R is transitive )
let R be Relation; :: thesis: ( R = id X implies ( R is reflexive & R is symmetric & R is antisymmetric & R is transitive ) )
assume A1: R = id X ; :: thesis: ( R is reflexive & R is symmetric & R is antisymmetric & R is transitive )
then A2: ( dom R = X & rng R = X ) by RELAT_1:45;
thus R is_reflexive_in field R :: according to RELAT_2:def 9 :: thesis: ( R is symmetric & R is antisymmetric & R is transitive )

proof

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in field R or [x,x] in R )
thus ( not x in field R or [x,x] in R ) by A1, A2, RELAT_1:def 10; :: thesis: verum

end;

thus R is_symmetric_in field R :: according to RELAT_2:def 11 :: thesis: ( R is antisymmetric & R is transitive )

proof

let x be set ; :: according to RELAT_2:def 3 :: thesis: for b₁ being set holds
( not x in field R or not b₁ in field R or not [x,b₁] in R or [b₁,x] in R )
let y be set ; :: thesis: ( not x in field R or not y in field R or not [x,y] in R or [y,x] in R )
assume that
x in field R and
y in field R ; :: thesis: ( not [x,y] in R or [y,x] in R )
assume [x,y] in R ; :: thesis: [y,x] in R
hence [y,x] in R by A1, RELAT_1:def 10; :: thesis: verum

end;

thus R is_antisymmetric_in field R :: according to RELAT_2:def 12 :: thesis: R is transitive

proof

let x be set ; :: according to RELAT_2:def 4 :: thesis: for b₁ being set holds
( not x in field R or not b₁ in field R or not [x,b₁] in R or not [b₁,x] in R or x = b₁ )
thus for b₁ being set holds
( not x in field R or not b₁ in field R or not [x,b₁] in R or not [b₁,x] in R or x = b₁ ) by A1, RELAT_1:def 10; :: thesis: verum

end;

thus R is_transitive_in field R :: according to RELAT_2:def 16 :: thesis: verum

proof

let x be set ; :: according to RELAT_2:def 8 :: thesis: for b₁, b₂ being set holds
( not x in field R or not b₁ in field R or not b₂ in field R or not [x,b₁] in R or not [b₁,b₂] in R or [x,b₂] in R )
thus for b₁, b₂ being set holds
( not x in field R or not b₁ in field R or not b₂ in field R or not [x,b₁] in R or not [b₁,b₂] in R or [x,b₂] in R ) by A1, RELAT_1:def 10; :: thesis: verum

end;