( not {{} } is empty & {{} } is Chain of W ) by Th22;
hence not for b₁ being Chain of W holds b₁ is empty ; :: thesis: verum