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