:: deftheorem defines satisfying_N7* NELSON_1:def 28 :
for L being non empty NelsonStr holds
( L is satisfying_N7* iff for a, b being Element of L holds b => (a "\/" b) = Top L );