let X, x, y be set ; :: thesis: ( x in Tarski-Class X & y in Tarski-Class X implies [x,y] in Tarski-Class X )
assume ( x in Tarski-Class X & y in Tarski-Class X ) ; :: thesis: [x,y] in Tarski-Class X
then ( {x,y} in Tarski-Class X & {x} in Tarski-Class X ) by Th26;
hence [x,y] in Tarski-Class X by Th26; :: thesis: verum