RelStr(# X,R #) is upper-bounded by Th8;
hence ( RelStr(# X,R #) is complete & RelStr(# X,R #) is connected & RelStr(# X,R #) is continuous & RelStr(# X,R #) is algebraic ) by Th9, Th11; :: thesis: verum