:: deftheorem Def7 defines CLbasis WAYBEL23:def 7 :
for L being continuous sup-Semilattice
for b₂ being Subset of L holds
( b₂ is CLbasis of L iff ( b₂ is join-closed & ( for x being Element of L holds x = sup ((waybelow x) /\ b₂) ) ) );