let T be Polish-language; :: thesis: for m, n being Nat
for a being object st a in T ^^ m & a in T ^^ n & not T is trivial holds
m = n
let m, n be Nat; :: thesis: for a being object st a in T ^^ m & a in T ^^ n & not T is trivial holds
m = n
let a be object ; :: thesis: ( a in T ^^ m & a in T ^^ n & not T is trivial implies m = n )
assume that
A1: ( a in T ^^ m & a in T ^^ n ) and
A2: not T is trivial ; :: thesis: m = n
reconsider T = T as non trivial Polish-language by A2;
( a in T ^^ m & a in T ^^ n ) by A1;
then ( m <= n & n <= m ) by Lm2;
hence m = n by XXREAL_0:1; :: thesis: verum