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