now

let Amp be AmpleSet of R; :: thesis: for x being Element of ex zz being Element of st
( zz in Amp & zz is_associated_to x )
let x be Element of ; :: thesis: ex zz being Element of 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 st
( zz in Amp & zz is_associated_to x ) ; :: thesis: verum

end;

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