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;