consider x being object such that
A1: x in the carrier of L by XBOOLE_0:def 1;
reconsider x = x as Element of L by A1;
take {x} -Ideal ; :: thesis: {x} -Ideal is finitely_generated
thus {x} -Ideal is finitely_generated ; :: thesis: verum