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