let seq be ExtREAL_sequence; :: thesis: inf seq <= sup seq
( inf seq <= seq . 0 & seq . 0 <= sup seq ) by Th23;
hence inf seq <= sup seq by XXREAL_0:2; :: thesis: verum