let G be Group; :: thesis: for A being Subset of G holds A |^ (1_ G) = A
let A be Subset of G; :: thesis: A |^ (1_ G) = A
thus A |^ (1_ G) = (((1_ G) ") * A) * (1_ G) by Th59
.= ((1_ G) ") * A by GROUP_2:37
.= (1_ G) * A by GROUP_1:8
.= A by GROUP_2:37 ; :: thesis: verum