let y, z be ExtReal; ( 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
; y = z
A8:
y <= z
by A5, A6;
z <= y
by A4, A7;
hence
y = z
by A8, XXREAL_0:1; verum