let L be transitive antisymmetric with_infima RelStr ; :: thesis: for a, b, c, d being Element of L st a <= c & b <= d holds
a "/\" b <= c "/\" d
let a, b, c, d be Element of L; :: thesis: ( a <= c & b <= d implies a "/\" b <= c "/\" d )
assume A1: ( a <= c & b <= d ) ; :: thesis: a "/\" b <= c "/\" d
A2: ex x being Element of L st
( c >= x & d >= x & ( for z being Element of L st c >= z & d >= z holds
x >= z ) ) by LATTICE3:def 11;
ex_inf_of {a,b},L by YELLOW_0:21;
then ( a "/\" b <= a & a "/\" b <= b ) by YELLOW_0:19;
then ( a "/\" b <= c & a "/\" b <= d ) by A1, ORDERS_2:26;
hence a "/\" b <= c "/\" d by A2, LATTICE3:def 14; :: thesis: verum