let L be upper-bounded Semilattice; :: thesis: InclPoset (Filt L) is complete
InclPoset (Ids (L opp)) is complete ;
hence InclPoset (Filt L) is complete by Th7; :: thesis: verum