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

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

end;

hence B1 misses B2 ; :: thesis: verum