let Y, X be set ; :: thesis: ( ( Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {} ) implies ( proj1 [:X,Y:] = X & proj2 [:Y,X:] = X ) )
set y = the Element of Y;
assume ( Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {} ) ; :: thesis: ( proj1 [:X,Y:] = X & proj2 [:Y,X:] = X )
then A1: Y <> {} by ZFMISC_1:90;

now

let x be set ; :: thesis: ( x in X iff ex y being set st [x,y] in [:X,Y:] )
( x in X implies [x, the Element of Y] in [:X,Y:] ) by A1, ZFMISC_1:87;
hence ( x in X iff ex y being set st [x,y] in [:X,Y:] ) by ZFMISC_1:87; :: thesis: verum

end;

hence proj1 [:X,Y:] = X by RELAT_1:def 4; :: thesis: proj2 [:Y,X:] = X

now

let x be set ; :: thesis: ( x in X iff ex y being set st [y,x] in [:Y,X:] )
( x in X implies [ the Element of Y,x] in [:Y,X:] ) by A1, ZFMISC_1:87;
hence ( x in X iff ex y being set st [y,x] in [:Y,X:] ) by ZFMISC_1:87; :: thesis: verum

end;

hence proj2 [:Y,X:] = X by RELAT_1:def 5; :: thesis: verum