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 Th43;
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 Th43;
assume {} is_>=_than b ; :: thesis: I >= b
b9 c= [#] L ;
hence I >= b by YELLOW_1:3; :: thesis: verum

end;

I is_<=_than {}

proof

let y be Element of (InclPoset (Ids L)); :: according to LATTICE3:def 8 :: thesis: ( not y in {} or I <= y )
assume y in {} ; :: thesis: I <= y
hence I <= y ; :: thesis: verum

end;

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