let L be non empty LATTICE; :: thesis: for x being Element of L
for A being Chain of x,x holds card A = 1
let x be Element of L; :: thesis: for A being Chain of x,x holds card A = 1
let A be Chain of x,x; :: thesis: card A = 1
for z being Element of L st z in A holds
z in {x}
proof
let z be Element of L; :: thesis: ( z in A implies z in {x} )
assume z in A ; :: thesis: z in {x}
then ( x <= z & z <= x ) by LATTICE7:def 2;
then z = x by ORDERS_2:2;
hence z in {x} by TARSKI:def 1; :: thesis: verum
end;
then A c= {x} by LATTICE7:def 1;
hence card A = 1 by CARD_2:42, ZFMISC_1:33; :: thesis: verum