theorem Th25: :: AFINSQ_2:25
for A, B1, B2 being set st B1 <N< B2 holds
A /\ B1 <N< A /\ B2