let x, y, z, X be set ; :: thesis: ( [x,y,z] in X implies y in proj2_3 X )
assume [x,y,z] in X ; :: thesis: y in proj2_3 X
then [x,y] in proj1 X by Def4;
hence y in proj2_3 X by Def5; :: thesis: verum