let y, z be ExtReal; :: 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

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 ; :: thesis: y = z

A16: z <= y by A13, A14;

y <= z by A12, A15;

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

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 ; :: thesis: y = z

A16: z <= y by A13, A14;

y <= z by A12, A15;

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