let R be non empty interval RelStr ; :: thesis: R is complete

for X being Subset of R holds ex_sup_of X,R by Th8;

hence R is complete by YELLOW_0:53; :: thesis: verum

for X being Subset of R holds ex_sup_of X,R by Th8;

hence R is complete by YELLOW_0:53; :: thesis: verum