let X be set ; :: thesis: ( id X is_reflexive_in X & id X is_symmetric_in X & id X is_transitive_in X )
thus for x being set st x in X holds
[x,x] in id X by RELAT_1:def 10; :: according to RELAT_2:def 1 :: thesis: ( id X is_symmetric_in X & id X is_transitive_in X )
thus for x, y being set st x in X & y in X & [x,y] in id X holds
[y,x] in id X by RELAT_1:def 10; :: according to RELAT_2:def 3 :: thesis: id X is_transitive_in X
thus for x, y, z being set st x in X & y in X & z in X & [x,y] in id X & [y,z] in id X holds
[x,z] in id X by RELAT_1:def 10; :: according to RELAT_2:def 8 :: thesis: verum