let x, y, z be object ; :: thesis: for X being set st [x,y,z] in X holds
x in proj1_3 X
let 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 Def12;
hence x in proj1_3 X by Def12; :: thesis: verum