let A, B1, B2 be set ; :: thesis: ( B1 <N< B2 implies A /\ B1 <N< A /\ B2 )
assume A0: B1 <N< B2 ; :: thesis: A /\ B1 <N< A /\ B2
for n, m being Nat st n in A /\ B1 & m in A /\ B2 holds
n < m

proof

let n, m be Nat; :: thesis: ( n in A /\ B1 & m in A /\ B2 implies n < m )
assume ( n in A /\ B1 & m in A /\ B2 ) ; :: thesis: n < m
then ( n in B1 & m in B2 ) by XBOOLE_0:def 4;
hence n < m by A0, AE100; :: thesis: verum

end;

hence A /\ B1 <N< A /\ B2 by AE100; :: thesis: verum