let E be set ; :: thesis: for A being Subset of (E ^omega) holds A + = A |^.. 1

let A be Subset of (E ^omega); :: thesis: A + = A |^.. 1

let A be Subset of (E ^omega); :: thesis: A + = A |^.. 1

A1: now :: thesis: for x being object st x in A + holds

x in A |^.. 1

x in A |^.. 1

let x be object ; :: thesis: ( x in A + implies x in A |^.. 1 )

assume x in A + ; :: thesis: x in A |^.. 1

then consider k being Nat such that

A2: 0 < k and

A3: x in A |^ k by Th48;

0 + 1 <= k by A2, NAT_1:13;

hence x in A |^.. 1 by A3, Th2; :: thesis: verum

end;assume x in A + ; :: thesis: x in A |^.. 1

then consider k being Nat such that

A2: 0 < k and

A3: x in A |^ k by Th48;

0 + 1 <= k by A2, NAT_1:13;

hence x in A |^.. 1 by A3, Th2; :: thesis: verum

now :: thesis: for x being object st x in A |^.. 1 holds

x in A +

hence
A + = A |^.. 1
by A1, TARSKI:2; :: thesis: verumx in A +

let x be object ; :: thesis: ( x in A |^.. 1 implies x in A + )

assume x in A |^.. 1 ; :: thesis: x in A +

then ex k being Nat st

( 1 <= k & x in A |^ k ) by Th2;

hence x in A + by Th48; :: thesis: verum

end;assume x in A |^.. 1 ; :: thesis: x in A +

then ex k being Nat st

( 1 <= k & x in A |^ k ) by Th2;

hence x in A + by Th48; :: thesis: verum