:: deftheorem Def1 defines CompactSublatt WAYBEL_8:def 1 :
for L being non empty reflexive RelStr
for b₂ being strict full SubRelStr of L holds
( b₂ = CompactSublatt L iff for x being Element of L holds
( x in the carrier of b₂ iff x is compact ) );