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 object ; :: 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 Def16;
hence x in dom (==_ X) by XTUPLE_0:def 12; :: thesis: verum
end;
A2: 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 object ; :: 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 A2;
assume [x,y] in ==_ X ; :: thesis: [y,x] in ==_ X
then s1 == s2 by Def16;
hence [y,x] in ==_ X by Def16; :: thesis: verum
end;
let x, y, z be object ; :: 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 A2;
assume ( [x,y] in ==_ X & [y,z] in ==_ X ) ; :: thesis: [x,z] in ==_ X
then ( s1 == s2 & s2 == s3 ) by Def16;
then s1 == s3 ;
hence [x,z] in ==_ X by Def16; :: thesis: verum