let R be non empty addLoopStr ; :: thesis: for I, J being Subset of
for K being add-closed Subset of st I c= K & J c= K holds
I + J c= K
let I, J be Subset of ; :: thesis: for K being add-closed Subset of st I c= K & J c= K holds
I + J c= K
let K be add-closed Subset of ; :: thesis: ( I c= K & J c= K implies I + J c= K )
assume A1: ( I c= K & J c= K ) ; :: thesis: I + J c= K

now

let u be set ; :: thesis: ( u in I + J implies u in K )
assume u in I + J ; :: thesis: u in K
then ex i, j being Element of st
( u = i + j & i in I & j in J ) ;
hence u in K by A1, Def1; :: thesis: verum

end;

hence I + J c= K by TARSKI:def 3; :: thesis: verum