let X be set ; :: thesis: ( proj1 X in bool (union (union X)) & proj2 X in bool (union (union X)) )

now :: thesis: ( proj1 X c= union (union X) & proj2 X c= union (union X) )

thus proj1 X c= union (union X) :: thesis: proj2 X c= union (union X)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in proj1 X or x in union (union X) )
assume x in proj1 X ; :: thesis: x in union (union X)
then ex y being object st [x,y] in X by XTUPLE_0:def 12;
hence x in union (union X) by XTUPLE_0:6; :: thesis: verum

end;

thus proj2 X c= union (union X) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in proj2 X or x in union (union X) )
assume x in proj2 X ; :: thesis: x in union (union X)
then ex y being object st [y,x] in X by XTUPLE_0:def 13;
hence x in union (union X) by XTUPLE_0:7; :: thesis: verum

end;

end;

hence ( proj1 X in bool (union (union X)) & proj2 X in bool (union (union X)) ) ; :: thesis: verum