theorem Th47: :: YELLOW_2:47

for L being with_suprema Poset holds
( ex_inf_of {} , InclPoset (Ids L) & "/\" ({},(InclPoset (Ids L))) = [#] L )