let L be transitive antisymmetric with_infima RelStr ; :: thesis: for a, b, c being Element of L st a <= b holds
a "/\" c <= b "/\" c
let a, b, c be Element of L; :: thesis: ( a <= b implies a "/\" c <= b "/\" c )
A1: a "/\" c <= a by YELLOW_0:23;
A2: a "/\" c <= c by YELLOW_0:23;
assume a <= b ; :: thesis: a "/\" c <= b "/\" c
then a "/\" c <= b by A1, YELLOW_0:def 2;
hence a "/\" c <= b "/\" c by A2, YELLOW_0:23; :: thesis: verum