now :: thesis: for Amp being AmpleSet of R
for x being Element of R ex zz being Element of R st
( zz in Amp & zz is_associated_to x )

let Amp be AmpleSet of R; :: thesis: for x being Element of R ex zz being Element of R st
( zz in Amp & zz is_associated_to x )
let x be Element of R; :: thesis: ex zz being Element of R st
( zz in Amp & zz is_associated_to x )
ex z being Element of Amp st z is_associated_to x by Th22;
hence ex zz being Element of R st
( zz in Amp & zz is_associated_to x ) ; :: thesis: verum

end;

hence ex b₁ being Element of R st
( b₁ in Amp & b₁ is_associated_to x ) ; :: thesis: verum