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 A1: ( X _c=^ Y & Y _c=^ Z ) ; :: thesis: X _c=^ Z
then ( X c=^ Y & Y c=^ Z ) by Def13;
then A2: X c=^ Z by Th60;
( X _c= Y & Y _c= Z ) by A1, Def13;
then X _c= Z by Th59;
hence X _c=^ Z by A2, Def13; :: thesis: verum