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 )
A1: x "/\" z <= x by YELLOW_0:23;
A2: x "/\" z <= z by YELLOW_0:23;
assume x <= y ; :: thesis: x "/\" z <= y "/\" z
then x "/\" z <= y by A1, ORDERS_2:3;
hence x "/\" z <= y "/\" z by A2, YELLOW_0:23; :: thesis: verum