let x, x1, x2, x3 be object ; :: thesis: for X being set st [x,x1,x2,x3] in X holds
x in proj1_4 X
let X be set ; :: thesis: ( [x,x1,x2,x3] in X implies x in proj1_4 X )
assume [x,x1,x2,x3] in X ; :: thesis: x in proj1_4 X
then [[x,x1],x2,x3] in X ;
then [x,x1] in proj1_3 X by Th13;
hence x in proj1_4 X by Def12; :: thesis: verum