let X be non empty set ; :: thesis: for Y being non empty Subset of ExtREAL
for F being Function of X,Y holds
( inf (- F) = - (sup F) & sup (- F) = - (inf F) )
let Y be non empty Subset of ExtREAL ; :: thesis: for F being Function of X,Y holds
( inf (- F) = - (sup F) & sup (- F) = - (inf F) )
let F be Function of X,Y; :: thesis: ( inf (- F) = - (sup F) & sup (- F) = - (inf F) )
thus inf (- F) = inf (- (rng F)) by Th37
.= - (sup F) by Th32 ; :: thesis: sup (- F) = - (inf F)
thus sup (- F) = sup (- (rng F)) by Th37
.= - (inf F) by Th33 ; :: thesis: verum