for A being non degenerated commutative Ring
for J being proper Ideal of A
for f being Element of A st not f in sqrt J holds
Ideals (A,J,f) has_upper_Zorn_property_wrt RelIncl (Ideals (A,J,f))