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: 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;

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

end;

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