let X, Y, Z be set ; :: thesis: ( Z c= [:X,Y:] implies ( proj1 Z c= X & proj2 Z c= Y ) )
assume Z c= [:X,Y:] ; :: thesis: ( proj1 Z c= X & proj2 Z c= Y )
then A1: ( proj1 Z c= proj1 [:X,Y:] & proj2 Z c= proj2 [:X,Y:] ) by XTUPLE_0:8, XTUPLE_0:9;
( proj1 [:X,Y:] c= X & proj2 [:X,Y:] c= Y ) by Th4;
hence ( proj1 Z c= X & proj2 Z c= Y ) by A1; :: thesis: verum