let X, Y, Z be set ; :: thesis: ( X c= Y & Y c= Z implies X c= Z )
assume that
A1: X c= Y and
A2: Y c= Z ; :: thesis: X c= Z
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Z )
assume x in X ; :: thesis: x in Z
then x in Y by A1, TARSKI:def 3;
hence x in Z by A2, TARSKI:def 3; :: thesis: verum