let y, z be ext-real number ; :: 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
Z1:
y is UpperBound of X
and
Z2:
for x being UpperBound of X holds y <= x
and
Z3:
z is UpperBound of X
and
Z4:
for x being UpperBound of X holds z <= x
; :: thesis: y = z
A:
z <= y
by Z1, Z4;
y <= z
by Z2, Z3;
hence
y = z
by A, XXREAL_0:1; :: thesis: verum