let k, n be Nat; :: thesis: ( k <= n implies k = k /\ n )
assume k <= n ; :: thesis: k = k /\ n
then Segm k c= Segm n by Th40;
hence k = k /\ n by XBOOLE_1:28; :: thesis: verum