:: deftheorem defines cyclic LATWAL_2:def 10 :
for L being WA-Lattice
for A being Subset of L holds
( A is cyclic iff A is_cycle_of L );