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 ( UAp X c= UAp Y & UAp Y c= UAp Z ) by Def12;
then UAp X c= UAp Z by XBOOLE_1:1;
hence X c=^ Z by Def12; :: thesis: verum