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