let E be set ; :: thesis: for A being Subset of holds A c= A *
let A be Subset of ; :: thesis: A c= A *
A = A |^ 1 by Th26;
hence A c= A * by Th43; :: thesis: verum