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 :: thesis: not B1 meets B2

set x = the Element of B1 /\ B2;
assume a2: B1 meets B2 ; :: thesis: contradiction
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; :: thesis: verum

end;

hence B1 misses B2 ; :: thesis: verum