for L being non empty NelsonStr st L is satisfying_N0* holds
( L is Nelson_Algebra iff ( L is satisfying_N1* & L is satisfying_N2* & L is satisfying_N3* & L is satisfying_N4* & L is satisfying_N5* & L is satisfying_N6* & L is satisfying_N7* & L is satisfying_N8* & L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* ) )