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