let x be object ; :: thesis: for X being set st x in proj2_4 X holds
ex x1, x2, x3 being object st [x1,x,x2,x3] in X
let X be set ; :: thesis: ( x in proj2_4 X implies ex x1, x2, x3 being object st [x1,x,x2,x3] in X )
assume x in proj2_4 X ; :: thesis: ex x1, x2, x3 being object st [x1,x,x2,x3] in X
then consider x1 being object such that
A1: [x1,x] in proj1_3 X by Def13;
consider x2 being object such that
A2: [[x1,x],x2] in proj1 X by A1, Def12;
consider x3 being object such that
A3: [[[x1,x],x2],x3] in X by A2, Def12;
take x1 ; :: thesis: ex x2, x3 being object st [x1,x,x2,x3] in X
take x2 ; :: thesis: ex x3 being object st [x1,x,x2,x3] in X
take x3 ; :: thesis: [x1,x,x2,x3] in X
thus [x1,x,x2,x3] in X by A3; :: thesis: verum