:: deftheorem defines Scott WAYBEL11:def 5 :
for T being non empty finite reflexive transitive antisymmetric with_suprema TopRelStr holds
( T is Scott iff for S being Subset of T holds
( S is open iff S is upper ) );