theorem Th63: :: IDEAL_1:63

for R being non empty add-cancelable add-associative right_zeroed well-unital distributive associative commutative left_zeroed doubleLoopStr
for F being non empty Subset of R holds
( F -Ideal = F -LeftIdeal & F -Ideal = F -RightIdeal )