let y, z be ext-real number ; :: thesis: ( y is LowerBound of X & ( for x being LowerBound of X holds x <= y ) & z is LowerBound of X & ( for x being LowerBound of X holds x <= z ) implies y = z )
assume that
Z1:
y is LowerBound of X
and
Z2:
for x being LowerBound of X holds x <= y
and
Z3:
z is LowerBound of X
and
Z4:
for x being LowerBound of X holds x <= z
; :: thesis: y = z
A:
y <= z
by Z1, Z4;
z <= y
by Z2, Z3;
hence
y = z
by A, XXREAL_0:1; :: thesis: verum