let k, n be Element of NAT ; :: thesis: ( k <= n implies k = k /\ n )
assume k <= n ; :: thesis: k = k /\ n
then k c= n by NAT_1:40;
hence k = k /\ n by XBOOLE_1:28; :: thesis: verum