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

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

end;

hence B1 misses B2 ; :: thesis: verum