:: Ring Ideals :: by Jonathan Backer , Piotr Rudnicki and Christoph Schwarzweller :: :: Received November 20, 2000 :: Copyright (c) 2000-2012 Association of Mizar Users
uniqueness
for b1, b2 being Ideal of L st F c= b1 & ( for I being Ideal of L st F c= I holds b1c= I ) & F c= b2 & ( for I being Ideal of L st F c= I holds b2c= I ) holds b1= b2