let X, x, y be set ; :: thesis: ( x in field (Total X) & y in field (Total X) implies [x,y] in Total X )
assume ( x in field (Total X) & y in field (Total X) ) ; :: thesis: [x,y] in Total X
then ( x in X & y in X ) by ORDERS_1:12;
hence [x,y] in Total X by Th2; :: thesis: verum