let V be non empty addLoopStr ; :: thesis: [#] V is having-inverse
for v being Element of V st v in [#] V holds
- v in [#] V ;
hence [#] V is having-inverse by Def1; :: thesis: verum