let L be with_suprema Poset; :: thesis: ( ex_inf_of {} , InclPoset (Ids L) & "/\" ({},(InclPoset (Ids L))) = [#] L )
set P = InclPoset (Ids L);
reconsider I = [#] L as Element of (InclPoset (Ids L)) by Th41;
A1: for b being Element of (InclPoset (Ids L)) st b is_<=_than {} holds
I >= b

proof

let b be Element of (InclPoset (Ids L)); :: thesis: ( b is_<=_than {} implies I >= b )
reconsider b9 = b as Ideal of L by Th41;
assume {} is_>=_than b ; :: thesis: I >= b
b9 c= [#] L ;
hence I >= b by YELLOW_1:3; :: thesis: verum

end;

I is_<=_than {} ;
hence ( ex_inf_of {} , InclPoset (Ids L) & "/\" ({},(InclPoset (Ids L))) = [#] L ) by A1, YELLOW_0:31; :: thesis: verum