:: deftheorem defines is_cycle_of LATWAL_2:def 9 :
for L being WA-Lattice
for A being set holds
( A is_cycle_of L iff for a, b being Element of L st a <> b & a in A & b in A holds
A = Segment (a,b) );