let A, B1, B2 be set ; :: thesis: ( B1 <N< B2 implies A /\ B1 <N< A /\ B2 )
assume A1: 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 that
A2: n in A /\ B1 and
A3: m in A /\ B2 ; :: thesis: n < m
A4: m in B2 by A3, XBOOLE_0:def 4;
n in B1 by A2, XBOOLE_0:def 4;
hence n < m by A1, A4; :: thesis: verum

end;

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