:: deftheorem Def16 defines -RightIdeal IDEAL_1:def 16 :
for L being non empty doubleLoopStr
for F being Subset of L st not F is empty holds
for b₃ being RightIdeal of L holds
( b₃ = F -RightIdeal iff ( F c= b₃ & ( for I being RightIdeal of L st F c= I holds
b₃ c= I ) ) );