let Z, X, Y 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 Th5;
( proj1 [:X,Y:] c= X & proj2 [:X,Y:] c= Y ) by Th12;
hence ( proj1 Z c= X & proj2 Z c= Y ) by A1, XBOOLE_1:1; :: thesis: verum