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