A1: {{} } is Chain of W by Th22;
thus not for b₁ being Chain of W holds b₁ is empty by A1; :: thesis: verum