for L being non empty RelStr st ( for A being Subset of L holds ex_inf_of A,L ) holds
L is complete