reconsider A = { the Element of L} as Subset of L by ZFMISC_1:31;
A is cyclic by SingleCycle;
hence ex b₁ being Subset of L st b₁ is cyclic ; :: thesis: verum