let a, b be Nat; :: thesis: ( Seg a = Seg b implies a = b )
assume Seg a = Seg b ; :: thesis: a = b
then ( a <= b & b <= a ) by Th7;
hence a = b by XXREAL_0:1; :: thesis: verum