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

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