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

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