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