for L being lower-bounded sup-Semilattice
for A being non empty Subset of (InclPoset (Ids L)) holds
( ex_inf_of A, InclPoset (Ids L) & inf A = meet A )