let x, X be set ; :: thesis: ( x in proj1_4 X implies ex x1, x2, x3 being set st [x,x1,x2,x3] in X )
assume x in proj1_4 X ; :: thesis: ex x1, x2, x3 being set st [x,x1,x2,x3] in X
then consider x1 being set such that
W1: [x,x1] in proj1_3 X by Def4;
consider x2 being set such that
W2: [[x,x1],x2] in proj1 X by W1, Def4;
consider x3 being set such that
W3: [[[x,x1],x2],x3] in X by W2, Def4;
take x1 ; :: thesis: ex x2, x3 being set st [x,x1,x2,x3] in X
take x2 ; :: thesis: ex x3 being set st [x,x1,x2,x3] in X
take x3 ; :: thesis: [x,x1,x2,x3] in X
thus [x,x1,x2,x3] in X by W3; :: thesis: verum