let B1, B2 be finite natural-membered set ; :: thesis: ( B1 <N< B2 implies B1 misses B2 )
assume A1: B1 <N< B2 ; :: thesis: B1 misses B2

now

assume B1 meets B2 ; :: thesis: contradiction
then B2: B1 /\ B2 <> {} by XBOOLE_0:def 7;
consider x being Element of B1 /\ B2;
( x in B1 & x in B2 ) by B2, XBOOLE_0:def 4;
hence contradiction by A1, AE100; :: thesis: verum

end;

hence B1 misses B2 ; :: thesis: verum