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 x9 = x, y9 = y as Ideal of L by Th41;
x9 /\ y9 is Ideal of L by Th40;
then x9 /\ y9 in { X where X is Ideal of L : verum } ;
hence x "/\" y = x /\ y by YELLOW_1:9; :: thesis: verum