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 A1: ( x in Tarski-Class X & y in Tarski-Class X ) ; :: thesis: [x,y] in Tarski-Class X
A2: ( {x,y} in Tarski-Class X & {x} in Tarski-Class X ) by A1, Th30;
thus [x,y] in Tarski-Class X by A2, Th30; :: thesis: verum