let E be set ; :: thesis: for A being Subset of holds <%> E in A *
let A be Subset of ; :: thesis: <%> E in A *
{(<%> E)} = A |^ 0 by Th25;
then <%> E in A |^ 0 by TARSKI:def 1;
hence <%> E in A * by Th42; :: thesis: verum