:: deftheorem Def7 defines Subalgebras WAYBEL10:def 7 :
for L being non empty RelStr
for b₂ being non empty strict full SubRelStr of ClosureSystems L holds
( b₂ = Subalgebras L iff for R being strict closure System of L holds
( R is Element of b₂ iff R is directed-sups-inheriting ) );