:: deftheorem Def26 defines len MODELC_3:def 26 :
for H being LTL-formula
for W being Subset of (Subformulae H)
for b₃ being Real holds
( b₃ = len W iff ex L being FinSequence st
( rng L = Subformulae H & L is one-to-one & b₃ = len (L,W) ) );