let L be non empty right_unital multLoopStr ; :: thesis: for S, T being Subset of L st 1. L in T holds
S c= S * T
let S, T be Subset of L; :: thesis: ( 1. L in T implies S c= S * T )
assume A: 1. L in T ; :: thesis: S c= S * T

now :: thesis: for x being object st x in S holds
x in S * T

let x be object ; :: thesis: ( x in S implies x in S * T )
assume B: x in S ; :: thesis: x in S * T
then reconsider a = x as Element of L ;
a * (1. L) in { (s1 * s2) where s1, s2 is Element of L : ( s1 in S & s2 in T ) } by A, B;
hence x in S * T ; :: thesis: verum

end;

hence S c= S * T ; :: thesis: verum