let G be Group; :: thesis: for A being Subset of G st A <> {} holds
(1_ G) |^ A = {(1_ G)}
let A be Subset of G; :: thesis: ( A <> {} implies (1_ G) |^ A = {(1_ G)} )
assume A1: A <> {} ; :: thesis: (1_ G) |^ A = {(1_ G)}
thus (1_ G) |^ A c= {(1_ G)} :: according to XBOOLE_0:def 10 :: thesis: {(1_ G)} c= (1_ G) |^ A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (1_ G) |^ A or x in {(1_ G)} )
assume x in (1_ G) |^ A ; :: thesis: x in {(1_ G)}
then ex a being Element of G st
( x = (1_ G) |^ a & a in A ) by Th51;
then x = 1_ G by Th22;
hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(1_ G)} or x in (1_ G) |^ A )
assume x in {(1_ G)} ; :: thesis: x in (1_ G) |^ A
then A2: x = 1_ G by TARSKI:def 1;
consider y being Element of A;
reconsider y = y as Element of G by A1, TARSKI:def 3;
(1_ G) |^ y = x by A2, Th22;
hence x in (1_ G) |^ A by A1, Th51; :: thesis: verum