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

c <= a

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

A1: a "/\" b <= a by YELLOW_0:23;

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

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

c <= a

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

A1: a "/\" b <= a by YELLOW_0:23;

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

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