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

now

assume B1: (B1 /\ B2) /\ NAT <> {} ; :: thesis: contradiction
consider x being Element of (B1 /\ B2) /\ NAT ;
B2: ( x in B1 /\ B2 & x in NAT ) by B1, XBOOLE_0:def 4;
reconsider nx = x as Nat ;
( nx in B1 & nx in B2 ) by B2, XBOOLE_0:def 4;
hence contradiction by AE100, A1; :: thesis: verum

end;

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