let E be set ; :: thesis: for A being Subset of holds A ^^ A c= A +
let A be Subset of ; :: thesis: A ^^ A c= A +
A ^^ A = A |^ 2 by FLANG_1:27;
hence A ^^ A c= A + by Th49; :: thesis: verum