let x1, x, x2, x3, X be set ; :: thesis: ( [x1,x,x2,x3] in X implies x in proj2_4 X )
assume [x1,x,x2,x3] in X ; :: thesis: x in proj2_4 X
then [[x1,x],x2,x3] in X ;
then [x1,x] in proj1_3 X by Th14a;
hence x in proj2_4 X by Def5; :: thesis: verum