let L be transitive antisymmetric with_infima RelStr ; :: thesis: for x, y, z being Element of L st x <= y holds
x "/\" z <= y "/\" z
let x, y, z be Element of L; :: thesis: ( x <= y implies x "/\" z <= y "/\" z )
assume A1: x <= y ; :: thesis: x "/\" z <= y "/\" z
x "/\" z <= x by YELLOW_0:23;
then ( x "/\" z <= y & x "/\" z <= z ) by A1, ORDERS_2:26, YELLOW_0:23;
hence x "/\" z <= y "/\" z by YELLOW_0:23; :: thesis: verum