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 <= i & i "/\" j <= j ) by YELLOW_0:23;
then ( i "/\" j in I & i "/\" j in J ) by WAYBEL_0:def 19;
hence I /\ J is Ideal of L by WAYBEL_0:27, WAYBEL_0:44, XBOOLE_0:def 4; :: thesis: verum