set R = ==_ X;
thus A1: dom (==_ X) = the carrier' of X :: according to PARTFUN1:def 2 :: thesis: ( ==_ X is symmetric & ==_ X is transitive )

proof

thus dom (==_ X) c= the carrier' of X ; :: according to XBOOLE_0:def 10 :: thesis: the carrier' of X c= dom (==_ X)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier' of X or x in dom (==_ X) )
assume x in the carrier' of X ; :: thesis: x in dom (==_ X)
then reconsider s = x as stack of X ;
[s,s] in ==_ X by REL;
hence x in dom (==_ X) by RELAT_1:def 4; :: thesis: verum

end;

A4: field (==_ X) = (dom (==_ X)) \/ (rng (==_ X))
.= the carrier' of X by A1, XBOOLE_1:12 ;
thus ==_ X is symmetric :: thesis: ==_ X is transitive

proof

let x, y be set ; :: according to RELAT_2:def 3,RELAT_2:def 11 :: thesis: ( not x in field (==_ X) or not y in field (==_ X) or not [x,y] in ==_ X or [y,x] in ==_ X )
assume ( x in field (==_ X) & y in field (==_ X) ) ; :: thesis: ( not [x,y] in ==_ X or [y,x] in ==_ X )
then reconsider s1 = x, s2 = y as stack of X by A4;
assume [x,y] in ==_ X ; :: thesis: [y,x] in ==_ X
then s1 == s2 by REL;
hence [y,x] in ==_ X by REL; :: thesis: verum

end;

let x, y, z be set ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: ( not x in field (==_ X) or not y in field (==_ X) or not z in field (==_ X) or not [x,y] in ==_ X or not [y,z] in ==_ X or [x,z] in ==_ X )
assume ( x in field (==_ X) & y in field (==_ X) & z in field (==_ X) ) ; :: thesis: ( not [x,y] in ==_ X or not [y,z] in ==_ X or [x,z] in ==_ X )
then reconsider s1 = x, s2 = y, s3 = z as stack of X by A4;
assume ( [x,y] in ==_ X & [y,z] in ==_ X ) ; :: thesis: [x,z] in ==_ X
then ( s1 == s2 & s2 == s3 ) by REL;
then s1 == s3 by Th41;
hence [x,z] in ==_ X by REL; :: thesis: verum