now :: thesis: for b, c being Real st b |^ n = a & b > 0 & c |^ n = a & c > 0 holds

not b <> c

hence
for bnot b <> c

let b, c be Real; :: thesis: ( b |^ n = a & b > 0 & c |^ n = a & c > 0 implies not b <> c )

assume that

A35: b |^ n = a and

A36: b > 0 and

A37: c |^ n = a and

A38: c > 0 and

A39: b <> c ; :: thesis: contradiction

end;assume that

A35: b |^ n = a and

A36: b > 0 and

A37: c |^ n = a and

A38: c > 0 and

A39: b <> c ; :: thesis: contradiction

per cases
( b > c or c > b )
by A39, XXREAL_0:1;

end;

( ( a > 0 & b