let x be object ; :: thesis: for X being set st x in proj1_3 X holds
ex y, z being object st [x,y,z] in X
let X be set ; :: thesis: ( x in proj1_3 X implies ex y, z being object st [x,y,z] in X )
assume x in proj1_3 X ; :: thesis: ex y, z being object st [x,y,z] in X
then consider y being object such that
A1: [x,y] in proj1 X by Def12;
consider z being object such that
A2: [[x,y],z] in X by A1, Def12;
take y ; :: thesis: ex z being object st [x,y,z] in X
take z ; :: thesis: [x,y,z] in X
thus [x,y,z] in X by A2; :: thesis: verum