let E be set ; :: thesis: for A being Subset of holds (A ? ) ^^ A = A |^ 1,2
let A be Subset of ; :: thesis: (A ? ) ^^ A = A |^ 1,2
A ? = A |^ 0 ,1 by Th79;
then (A ? ) ^^ A = A |^ (0 + 1),(1 + 1) by Th38;
hence (A ? ) ^^ A = A |^ 1,2 ; :: thesis: verum