let L be non empty reflexive antisymmetric with_infima RelStr ; :: thesis: ( L is distributive implies L is modular )

assume A1: L is distributive ; :: thesis: L is modular

assume A1: L is distributive ; :: thesis: L is modular

now :: thesis: for a, b, c being Element of L st a <= c holds

a "\/" (b "/\" c) = (a "\/" b) "/\" c

hence
L is modular
; :: thesis: veruma "\/" (b "/\" c) = (a "\/" b) "/\" c

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

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

hence a "\/" (b "/\" c) = (a "/\" c) "\/" (b "/\" c) by YELLOW_0:25

.= (a "\/" b) "/\" c by A1 ;

:: thesis: verum

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

hence a "\/" (b "/\" c) = (a "/\" c) "\/" (b "/\" c) by YELLOW_0:25

.= (a "\/" b) "/\" c by A1 ;

:: thesis: verum