theorem :: MCART_1:92

for x1, x2, x3 being object holds proj1 (proj1 {[x1,x2,x3]}) = {x1}