let R be non empty well-unital associative multLoopStr ; :: thesis: for Amp being AmpleSet of R holds
( 1. R in Amp & ( for a being Element of R ex z being Element of Amp st z is_associated_to a ) & ( for x, y being Element of Amp st x <> y holds
x is_not_associated_to y ) )
let Amp be AmpleSet of R; :: thesis: ( 1. R in Amp & ( for a being Element of R ex z being Element of Amp st z is_associated_to a ) & ( for x, y being Element of Amp st x <> y holds
x is_not_associated_to y ) )
Amp is Am of R by Def8;
hence ( 1. R in Amp & ( for a being Element of R ex z being Element of Amp st z is_associated_to a ) & ( for x, y being Element of Amp st x <> y holds
x is_not_associated_to y ) ) by Def7, Def8; :: thesis: verum