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