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