let E, x be set ; :: thesis: for A being Subset of (E ^omega) st A + = {x} holds

x = <%> E

let A be Subset of (E ^omega); :: thesis: ( A + = {x} implies x = <%> E )

assume that

A1: A + = {x} and

A2: x <> <%> E ; :: thesis: contradiction

A |^.. 1 = {x} by A1, Th50;

hence contradiction by A2, Th38; :: thesis: verum

x = <%> E

let A be Subset of (E ^omega); :: thesis: ( A + = {x} implies x = <%> E )

assume that

A1: A + = {x} and

A2: x <> <%> E ; :: thesis: contradiction

A |^.. 1 = {x} by A1, Th50;

hence contradiction by A2, Th38; :: thesis: verum