let E be set ; :: thesis: for A being Subset of holds A + = (A * ) ^^ A
let A be Subset of ; :: thesis: A + = (A * ) ^^ A
(A * ) ^^ A = A |^.. 1 by Th30;
hence A + = (A * ) ^^ A by Th50; :: thesis: verum