theorem Th6: :: FUNCT_5:12

for x, y being object holds
( proj1 {[x,y]} = {x} & proj2 {[x,y]} = {y} )