let y, z be ExtReal; :: thesis: ( y is UpperBound of X & ( for x being UpperBound of X holds y <= x ) & z is UpperBound of X & ( for x being UpperBound of X holds z <= x ) implies y = z )

assume that

A4: y is UpperBound of X and

A5: for x being UpperBound of X holds y <= x and

A6: z is UpperBound of X and

A7: for x being UpperBound of X holds z <= x ; :: thesis: y = z

A8: y <= z by A5, A6;

z <= y by A4, A7;

hence y = z by A8, XXREAL_0:1; :: thesis: verum

assume that

A4: y is UpperBound of X and

A5: for x being UpperBound of X holds y <= x and

A6: z is UpperBound of X and

A7: for x being UpperBound of X holds z <= x ; :: thesis: y = z

A8: y <= z by A5, A6;

z <= y by A4, A7;

hence y = z by A8, XXREAL_0:1; :: thesis: verum