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