let y, z be ExtReal; ( 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
A12:
y is LowerBound of X
and
A13:
for x being LowerBound of X holds x <= y
and
A14:
z is LowerBound of X
and
A15:
for x being LowerBound of X holds x <= z
; y = z
A16:
z <= y
by A13, A14;
y <= z
by A12, A15;
hence
y = z
by A16, XXREAL_0:1; verum