let L be Lattice; :: thesis: for P being non empty ClosedSubset of L st L is distributive holds
latt L,P is distributive
let P be non empty ClosedSubset of L; :: thesis: ( L is distributive implies latt L,P is distributive )
assume A1: for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) ; :: according to LATTICES:def 11 :: thesis: latt L,P is distributive
let a', b', c' be Element of (latt L,P); :: according to LATTICES:def 11 :: thesis: a' "/\" (b' "\/" c') = (a' "/\" b') "\/" (a' "/\" c')
reconsider a = a', b = b', c = c', bc = b' "\/" c', ab = a' "/\" b', ac = a' "/\" c' as Element of L by Th69;
thus a' "/\" (b' "\/" c') = a "/\" bc by Th74
.= a "/\" (b "\/" c) by Th74
.= (a "/\" b) "\/" (a "/\" c) by A1
.= ab "\/" (a "/\" c) by Th74
.= ab "\/" ac by Th74
.= (a' "/\" b') "\/" (a' "/\" c') by Th74 ; :: thesis: verum