{(Bottom L)} is Chain of L by ORDERS_2:8;
hence not for b₁ being Chain of L holds b₁ is empty ; :: thesis: verum