let L be transitive antisymmetric with_infima RelStr ; 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; ( a <= c & b <= d implies a "/\" b <= c "/\" d )
assume that
A1:
a <= c
and
A2:
b <= d
; 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; verum