let L be transitive antisymmetric with_suprema with_infima RelStr ; :: thesis: for a, b, c being Element of L holds a "/\" b <= a "\/" c
let a, b, c be Element of L; :: thesis: a "/\" b <= a "\/" c
( a "/\" b <= a & a <= a "\/" c ) by YELLOW_0:22, YELLOW_0:23;
hence a "/\" b <= a "\/" c by YELLOW_0:def 2; :: thesis: verum