let x1, x2, x3 be object ; :: thesis: proj1 (proj1 {[x1,x2,x3]}) = {x1}
thus proj1 (proj1 {[x1,x2,x3]}) = proj1 {[x1,x2]} by RELAT_1:9
.= {x1} by RELAT_1:9 ; :: thesis: verum