:: deftheorem Def1 defines Open WAYBEL_6:def 1 :
for L being non empty reflexive RelStr
for X being Subset of L holds
( X is Open iff for x being Element of L st x in X holds
ex y being Element of L st
( y in X & y << x ) );