let O be set ; :: thesis: for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st not s1 is empty & s2 is_finer_than s1 holds
not s2 is empty
let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st not s1 is empty & s2 is_finer_than s1 holds
not s2 is empty
let s1, s2 be CompositionSeries of G; :: thesis: ( not s1 is empty & s2 is_finer_than s1 implies not s2 is empty )
assume A1: not s1 is empty ; :: thesis: ( not s2 is_finer_than s1 or not s2 is empty )
assume s2 is_finer_than s1 ; :: thesis: not s2 is empty
then ex i being Nat st len s2 = (len s1) + i by Th95;
hence not s2 is empty by A1; :: thesis: verum