:: deftheorem Def1 defines lower WAYBEL19:def 1 :
for T being non empty TopRelStr holds
( T is lower iff { ((uparrow x) `) where x is Element of T : verum } is prebasis of T );