for X being set holds
( id X is_reflexive_in X & id X is_symmetric_in X & id X is_transitive_in X ) by RELAT_1:def 10;