let x, X be set ; :: thesis: ( x in proj2_3 X implies ex y, z being set st [y,x,z] in X )
assume x in proj2_3 X ; :: thesis: ex y, z being set st [y,x,z] in X
then consider y being set such that
W1: [y,x] in proj1 X by Def5;
consider z being set such that
W2: [[y,x],z] in X by W1, Def4;
take y ; :: thesis: ex z being set st [y,x,z] in X
take z ; :: thesis: [y,x,z] in X
thus [y,x,z] in X by W2; :: thesis: verum