let A be Tolerance_Space; :: thesis: for X, Y, Z being Subset of A st X _c=^ Y & Y _c=^ Z holds
X _c=^ Z
let X, Y, Z be Subset of A; :: thesis: ( X _c=^ Y & Y _c=^ Z implies X _c=^ Z )
assume ( X _c=^ Y & Y _c=^ Z ) ; :: thesis: X _c=^ Z
then ( X _c= Y & Y _c= Z & X c=^ Y & Y c=^ Z ) by Def13;
then ( X _c= Z & X c=^ Z ) by Th59, Th60;
hence X _c=^ Z by Def13; :: thesis: verum