let X, x, y be set ; :: thesis: ( x in X & y in X implies [x,y] in Total X )
assume ( x in X & y in X ) ; :: thesis: [x,y] in Total X
then [x,y] in [:X,X:] by ZFMISC_1:87;
hence [x,y] in Total X by EQREL_1:def 1; :: thesis: verum