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