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 )
thus R is_reflexive_in field R by A1, RELAT_1:def 10; :: according to RELAT_2:def 9 :: thesis: ( R is symmetric & R is antisymmetric & R is transitive )
thus R is_symmetric_in field R by A1, RELAT_1:def 10; :: according to RELAT_2:def 11 :: thesis: ( R is antisymmetric & R is transitive )
thus R is_antisymmetric_in field R by A1, RELAT_1:def 10; :: according to RELAT_2:def 12 :: thesis: R is transitive
thus R is_transitive_in field R by A1, RELAT_1:def 10; :: according to RELAT_2:def 16 :: thesis: verum