A1: for x, y being set st x in I & y in I & not x c= y holds
y c= x by XBOOLE_0:def 9, ORDINAL1:15;
now :: thesis: for x being ext-real object st x in I holds
x <= union I
let x be ext-real object ; :: thesis: ( x in I implies x <= union I )
assume A3: x in I ; :: thesis: x <= union I
then reconsider a = x as Nat ;
( Segm a = x & Segm (union I) = union I ) ;
hence x <= union I by A3, ZFMISC_1:74, NAT_1:39; :: thesis: verum
end;
hence max I = union I by A1, XXREAL_2:def 8, CARD_2:62; :: thesis: verum