theorem Th28: :: YELLOW_2:28

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