for x, y being set st x in Ids L & y in Ids L holds
x /\ y in Ids L

proof

let x, y be set ; :: thesis: ( x in Ids L & y in Ids L implies x /\ y in Ids L )
assume A1: ( x in Ids L & y in Ids L ) ; :: thesis: x /\ y in Ids L
then consider I being Ideal of L such that
A2: I = x ;
consider J being Ideal of L such that
A3: J = y by A1;
I /\ J is Ideal of L by Th42;
hence x /\ y in Ids L by A2, A3; :: thesis: verum

end;

hence InclPoset (Ids L) is with_infima by YELLOW_1:12; :: thesis: verum