theorem Th25: :: YELLOW_2:25

for L being non empty RelStr st ( for X being set holds ex_inf_of X,L ) holds
L is complete