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 Th18
.= - (sup F) by Th13 ; :: thesis: sup (- F) = - (inf F)
thus sup (- F) = sup (- (rng F)) by Th18
.= - (inf F) by Th14 ; :: thesis: verum