let L be Lattice; :: thesis: for p, q being Element of L
for H being Filter of L st p in H holds
( p "\/" q in H & q "\/" p in H )
let p, q be Element of L; :: thesis: for H being Filter of L st p in H holds
( p "\/" q in H & q "\/" p in H )
let H be Filter of L; :: thesis: ( p in H implies ( p "\/" q in H & q "\/" p in H ) )
( p [= p "\/" q & p "\/" q = q "\/" p ) by LATTICES:22;
hence ( p in H implies ( p "\/" q in H & q "\/" p in H ) ) by Th9; :: thesis: verum