let c, a be Nat; :: thesis: ( c <= a implies Seg c = (Seg a) /\ (Seg c) )
assume c <= a ; :: thesis: Seg c = (Seg a) /\ (Seg c)
then Seg c c= Seg a by Th7;
hence Seg c = (Seg a) /\ (Seg c) by XBOOLE_1:28; :: thesis: verum