let L be WA-Lattice; :: thesis: for a being Element of L holds {a} is_cycle_of L
let a be Element of L; :: thesis: {a} is_cycle_of L
set A = {a};
for x, y being Element of L st x <> y & x in {a} & y in {a} holds
{a} = Segment (x,y)

proof

let x, y be Element of L; :: thesis: ( x <> y & x in {a} & y in {a} implies {a} = Segment (x,y) )
assume A1: ( x <> y & x in {a} & y in {a} ) ; :: thesis: {a} = Segment (x,y)
then ( x = a & y = a ) by TARSKI:def 1;
hence {a} = Segment (x,y) by A1; :: thesis: verum

end;

hence {a} is_cycle_of L ; :: thesis: verum