let L be transitive antisymmetric with_suprema with_infima RelStr ; :: thesis: for a, b, c being Element of L st a <= c holds

a \ b <= c

let a, b, c be Element of L; :: thesis: ( a <= c implies a \ b <= c )

A1: a "/\" ('not' b) <= a by YELLOW_0:23;

assume a <= c ; :: thesis: a \ b <= c

hence a \ b <= c by A1, YELLOW_0:def 2; :: thesis: verum

a \ b <= c

let a, b, c be Element of L; :: thesis: ( a <= c implies a \ b <= c )

A1: a "/\" ('not' b) <= a by YELLOW_0:23;

assume a <= c ; :: thesis: a \ b <= c

hence a \ b <= c by A1, YELLOW_0:def 2; :: thesis: verum