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