let A be Chain of L; :: thesis: A is finite

per cases ( not A is empty or A is empty ) ;

suppose A1: not A is empty ; :: thesis: A is finite

then reconsider LL = L as non empty Poset ;
reconsider AA = A as non empty Chain of LL by A1;
ex a being Element of LL st
( AA = {a} or AA = {(Bottom LL),a} ) by Thflat01;
hence A is finite ; :: thesis: verum

end;

suppose A is empty ; :: thesis: A is finite

hence A is finite ; :: thesis: verum

end;

end;