theorem Th3: :: FUNCT_5:9

for X, Y being set st ( Y <> {} or [:X,Y:] <> {} or [:Y,X:] <> {} ) holds
( proj1 [:X,Y:] = X & proj2 [:Y,X:] = X )