:: deftheorem Def3 defines ClosureSystems WAYBEL10:def 3 :
for L being non empty RelStr
for b₂ being non empty strict full SubRelStr of Sub L holds
( b₂ = ClosureSystems L iff for R being strict SubRelStr of L holds
( R is Element of b₂ iff ( R is infs-inheriting & R is full ) ) );