let L be lower-bounded sup-Semilattice; :: thesis: InclPoset (Ids L) is complete
set P = InclPoset (Ids L);
for A being Subset of (InclPoset (Ids L)) holds ex_inf_of A, InclPoset (Ids L)

proof

let A be Subset of (InclPoset (Ids L)); :: thesis: ex_inf_of A, InclPoset (Ids L)

per cases ( A = {} or A <> {} ) ;

suppose A = {} ; :: thesis: ex_inf_of A, InclPoset (Ids L)

hence ex_inf_of A, InclPoset (Ids L) by Th47; :: thesis: verum

end;

suppose A <> {} ; :: thesis: ex_inf_of A, InclPoset (Ids L)

hence ex_inf_of A, InclPoset (Ids L) by Th46; :: thesis: verum

end;

end;

end;

hence InclPoset (Ids L) is complete by Th28; :: thesis: verum