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 ( LAp X c= LAp Y & LAp Y c= LAp Z ) ;
then LAp X c= LAp Z ;
hence X _c= Z ; :: thesis: verum