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 a9, b9, c9 be Element of (latt L,P); :: according to LATTICES:def 11 :: thesis: a9 "/\" (b9 "\/" c9) = (a9 "/\" b9) "\/" (a9 "/\" c9)
reconsider a = a9, b = b9, c = c9, bc = b9 "\/" c9, ab = a9 "/\" b9, ac = a9 "/\" c9 as Element of L by Th69;
thus a9 "/\" (b9 "\/" c9) = a "/\" bc by Th74
.= a "/\" (b "\/" c) by Th74
.= (a "/\" b) "\/" (a "/\" c) by A1
.= ab "\/" (a "/\" c) by Th74
.= ab "\/" ac by Th74
.= (a9 "/\" b9) "\/" (a9 "/\" c9) by Th74 ; :: thesis: verum