theorem Th18: :: WAYBEL_6:18

for L being lower-bounded continuous LATTICE
for X being Subset of L st X = (IRR L) \ {(Top L)} holds
X is order-generating