let B1, B2 be set ; :: thesis: ( B1 <N< B2 implies (B1 /\ B2) /\ NAT = {} )
assume A1: B1 <N< B2 ; :: thesis: (B1 /\ B2) /\ NAT = {}

now :: thesis: not (B1 /\ B2) /\ NAT <> {}

set x = the Element of (B1 /\ B2) /\ NAT;
reconsider nx = the Element of (B1 /\ B2) /\ NAT as Nat ;
assume (B1 /\ B2) /\ NAT <> {} ; :: thesis: contradiction
then A2: the Element of (B1 /\ B2) /\ NAT in B1 /\ B2 by XBOOLE_0:def 4;
then A3: nx in B2 by XBOOLE_0:def 4;
nx in B1 by A2, XBOOLE_0:def 4;
hence contradiction by A1, A3; :: thesis: verum

end;

hence (B1 /\ B2) /\ NAT = {} ; :: thesis: verum