let H be LTL-formula; :: thesis: for W being Subset of holds len W >= 0
let W be Subset of ; :: thesis: len W >= 0

now

per cases ( W = {} H or W <> {} H ) ;

suppose W = {} H ; :: thesis: len W >= 0

hence len W >= 0 by Th13; :: thesis: verum

end;

suppose W <> {} H ; :: thesis: len W >= 0

hence len W >= 0 by Th16; :: thesis: verum

end;

end;

end;

hence len W >= 0 ; :: thesis: verum