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 b1 being Element of R st
( b1 in Amp & b1 is_associated_to x ) ; :: thesis: verum