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