let L be with_infima Poset; :: thesis: for I, J being Ideal of L holds I /\ J is Ideal of L
let I, J be Ideal of L; :: thesis: I /\ J is Ideal of L
consider i being Element of I, j being Element of J;
set a = i "/\" j;
i "/\" j <= j by YELLOW_0:23;
then A1: i "/\" j in J by WAYBEL_0:def 19;
i "/\" j <= i by YELLOW_0:23;
then i "/\" j in I by WAYBEL_0:def 19;
hence I /\ J is Ideal of L by A1, WAYBEL_0:27, WAYBEL_0:44, XBOOLE_0:def 4; :: thesis: verum