theorem :: MCART_1:91

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