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 that
A1: a <= c and
A2: b <= d ; :: thesis: a "/\" b <= c "/\" d
A3: ex_inf_of {a,b},L by YELLOW_0:21;
then a "/\" b <= b by YELLOW_0:19;
then A4: a "/\" b <= d by A2, ORDERS_2:3;
a "/\" b <= a by A3, YELLOW_0:19;
then ( 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 ) ) & a "/\" b <= c ) by A1, LATTICE3:def 11, ORDERS_2:3;
hence a "/\" b <= c "/\" d by A4, LATTICE3:def 14; :: thesis: verum