let R be non empty addLoopStr ; :: thesis: for I, J being Subset of R
for K being add-closed Subset of R st I c= K & J c= K holds
I + J c= K
let I, J be Subset of R; :: thesis: for K being add-closed Subset of R st I c= K & J c= K holds
I + J c= K
let K be add-closed Subset of R; :: 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
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in I + J or u in K )
assume u in I + J ; :: thesis: u in K
then ex i, j being Element of R st
( u = i + j & i in I & j in J ) ;
hence u in K by A1, Def1; :: thesis: verum