let x, x1, x2, x3 be object ; :: thesis: for X being set st [x1,x,x2,x3] in X holds
x in proj2_4 X
let 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 Th13;
hence x in proj2_4 X by Def13; :: thesis: verum