let x, y be ExtReal; :: thesis: ( y is LowerBound of {x} iff y <= x )

x in {x} by TARSKI:def 1;

hence ( y is LowerBound of {x} implies y <= x ) by Def2; :: thesis: ( y <= x implies y is LowerBound of {x} )

assume A1: y <= x ; :: thesis: y is LowerBound of {x}

let z be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( z in {x} implies y <= z )

assume z in {x} ; :: thesis: y <= z

hence y <= z by A1, TARSKI:def 1; :: thesis: verum

x in {x} by TARSKI:def 1;

hence ( y is LowerBound of {x} implies y <= x ) by Def2; :: thesis: ( y <= x implies y is LowerBound of {x} )

assume A1: y <= x ; :: thesis: y is LowerBound of {x}

let z be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( z in {x} implies y <= z )

assume z in {x} ; :: thesis: y <= z

hence y <= z by A1, TARSKI:def 1; :: thesis: verum