let y be ExtReal; :: thesis: ( y = sup X iff ( y in X & ( for x being ExtReal st x in X holds

x <= y ) ) )

thus ( y = max X implies ( y in X & ( for x being ExtReal st x in X holds

x <= y ) ) ) by Def6, Th4; :: thesis: ( y in X & ( for x being ExtReal st x in X holds

x <= y ) implies y = sup X )

assume that

A1: y in X and

A2: for x being ExtReal st x in X holds

x <= y ; :: thesis: y = sup X

A3: for x being UpperBound of X holds y <= x by A1, Def1;

y is UpperBound of X by A2, Def1;

hence y = sup X by A3, Def3; :: thesis: verum

x <= y ) ) )

thus ( y = max X implies ( y in X & ( for x being ExtReal st x in X holds

x <= y ) ) ) by Def6, Th4; :: thesis: ( y in X & ( for x being ExtReal st x in X holds

x <= y ) implies y = sup X )

assume that

A1: y in X and

A2: for x being ExtReal st x in X holds

x <= y ; :: thesis: y = sup X

A3: for x being UpperBound of X holds y <= x by A1, Def1;

y is UpperBound of X by A2, Def1;

hence y = sup X by A3, Def3; :: thesis: verum