:: deftheorem defines maximal RING_1:def 4 :
for R being non empty doubleLoopStr
for I being Subset of R holds
( I is maximal iff ( I is proper & I is quasi-maximal ) );