let seq be ExtREAL_sequence; :: thesis: inf seq <= sup seq
A1: seq . 0 <= sup seq by Th23;
inf seq <= seq . 0 by Th23;
hence inf seq <= sup seq by A1, XXREAL_0:2; :: thesis: verum