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