let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for A being non-empty finite-yielding MSAlgebra of IIG
for v being SortSymbol of IIG holds size (v,A) > 0
let A be non-empty finite-yielding MSAlgebra of IIG; :: thesis: for v being SortSymbol of IIG holds size (v,A) > 0
let v be SortSymbol of IIG; :: thesis: size (v,A) > 0
consider s being non empty finite Subset of NAT such that
A1: s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } and
A2: size (v,A) = max s by Def4;
reconsider Y = s as non empty finite real-membered set ;
max Y in { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } by A1, XXREAL_2:def 8;
then ex t being Element of the Sorts of (FreeEnv A) . v st card t = max Y ;
hence size (v,A) > 0 by A2; :: thesis: verum