A1: {} is Chain of G by Lm1;
thus ex b₁ being Chain of G st b₁ is empty by A1; :: thesis: verum