not for L being Chain of P holds L is empty

proof

consider z being Element of P;
set IT = {z};
reconsider IT = {z} as Chain of P by ORDERS_2:35;
not IT is empty ;
hence not for L being Chain of P holds L is empty ; :: thesis: verum

end;

hence not for b₁ being Chain of P holds b₁ is empty ; :: thesis: verum