let L be Lattice; :: thesis: for F being Filter of L st L is modular holds
latt F is modular
let F be Filter of L; :: thesis: ( L is modular implies latt F is modular )
assume A1: for a, b, c being Element of L st a [= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c ; :: according to LATTICES:def 12 :: thesis: latt F is modular
let a, b, c be Element of (latt F); :: according to LATTICES:def 12 :: thesis: ( not a [= c or a "\/" (b "/\" c) = (a "\/" b) "/\" c )
assume A2: a [= c ; :: thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" c
reconsider p = a, q = b, r = c as Element of F by Th49;
b "/\" c = q "/\" r by Th50;
then A3: a "\/" (b "/\" c) = p "\/" (q "/\" r) by Th50;
a "\/" b = p "\/" q by Th50;
then A4: (a "\/" b) "/\" c = (p "\/" q) "/\" r by Th50;
p [= r by A2, Th51;
hence a "\/" (b "/\" c) = (a "\/" b) "/\" c by A1, A3, A4; :: thesis: verum