:: deftheorem defines with_top WAYBEL23:def 9 :
for L being non empty RelStr
for S being Subset of L holds
( S is with_top iff Top L in S );