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 that
A1: x in Ids L and
A2: y in Ids L ; :: thesis: x /\ y in Ids L
consider I being Ideal of L such that
A3: I = x by A1;
consider J being Ideal of L such that
A4: J = y by A2;
I /\ J is Ideal of L by Th40;
hence x /\ y in Ids L by A3, A4; :: thesis: verum

end;

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