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 by LATTICES:5;
hence ( p in H implies ( p "\/" q in H & q "\/" p in H ) ) by Th9; :: thesis: verum