let L be with_infima Poset; :: thesis: for x, y being Element of holds x "/\" y = x /\ y
let x, y be Element of ; :: 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