let S be non empty addLoopStr ; :: thesis: for v being Element of S holds v + ({} S) = {} S
let v be Element of S; :: thesis: v + ({} S) = {} S
assume v + ({} S) <> {} S ; :: thesis: contradiction
then consider x being object such that
A1: x in v + ({} S) by XBOOLE_0:def 1;
ex w being Element of S st
( x = v + w & w in {} S ) by A1;
hence contradiction ; :: thesis: verum