not for L being Chain of P holds L is empty

proof

set z = the Element of P;
set IT = { the Element of P};
reconsider IT = { the Element of P} as Chain of P by ORDERS_2:8;
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