let L be with_infima Poset; :: thesis: for x, y being Element of (InclPoset (Ids L)) holds x "/\" y = x /\ y
let x, y be Element of (InclPoset (Ids L)); :: thesis: x "/\" y = x /\ y
reconsider x' = x, y' = y as Ideal of L by Th43;
x' /\ y' is Ideal of L by Th42;
then x' /\ y' in { X where X is Ideal of L : verum } ;
hence x /\ y = x "/\" y by YELLOW_1:9; :: thesis: verum