let R be non empty doubleLoopStr ; :: thesis: for a being Element of R holds a in {a} -Ideal
let a be Element of R; :: thesis: a in {a} -Ideal
( a in {a} & {a} c= {a} -Ideal ) by Def14, TARSKI:def 1;
hence a in {a} -Ideal ; :: thesis: verum