let L be Lattice; :: thesis: for p being Element of L holds [#p,p#] = {p}
let p be Element of L; :: thesis: [#p,p#] = {p}
let q be Element of L; :: according to FILTER_2:def 1 :: thesis: ( q in [#p,p#] iff q in {p} )

hereby :: thesis: ( q in {p} implies q in [#p,p#] )

assume q in [#p,p#] ; :: thesis: q in {p}
then ( p [= q & q [= p ) by Th62;
then q = p by LATTICES:8;
hence q in {p} by TARSKI:def 1; :: thesis: verum

end;

p in [#p,p#] by Th62;
hence ( q in {p} implies q in [#p,p#] ) by TARSKI:def 1; :: thesis: verum