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
set i = the Element of I;
set j = the Element of J;
set a = the Element of I "/\" the Element of J;
the Element of I "/\" the Element of J <= the Element of J by YELLOW_0:23;
then A1: the Element of I "/\" the Element of J in J by WAYBEL_0:def 19;
the Element of I "/\" the Element of J <= the Element of I by YELLOW_0:23;
then the Element of I "/\" the Element of 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