let L be Lattice; :: thesis: for F being Filter of L st L is distributive holds
latt F is distributive
let F be Filter of L; :: thesis: ( L is distributive implies latt F is distributive )
assume A1: for p, q, r being Element of L holds p "/\" (q "\/" r) = (p "/\" q) "\/" (p "/\" r) ; :: according to LATTICES:def 11 :: thesis: latt F is distributive
let p9, q9, r9 be Element of (latt F); :: according to LATTICES:def 11 :: thesis: p9 "/\" (q9 "\/" r9) = (p9 "/\" q9) "\/" (p9 "/\" r9)
reconsider p = p9, q = q9, r = r9, qr = q9 "\/" r9 as Element of F by Th49;
A2: ( p9 "/\" q9 = p "/\" q & p9 "/\" r9 = p "/\" r ) by Th50;
thus p9 "/\" (q9 "\/" r9) = p "/\" qr by Th50
.= p "/\" (q "\/" r) by Th50
.= (p "/\" q) "\/" (p "/\" r) by A1
.= (p9 "/\" q9) "\/" (p9 "/\" r9) by A2, Th50 ; :: thesis: verum