let L be Lattice; :: thesis: for p, q, r being Element of L st p [= q holds
( r in [#p,q#] iff ( p [= r & r [= q ) )
let p, q, r be Element of L; :: thesis: ( p [= q implies ( r in [#p,q#] iff ( p [= r & r [= q ) ) )
assume p [= q ; :: thesis: ( r in [#p,q#] iff ( p [= r & r [= q ) )
then [#p,q#] = { s where s is Element of L : ( p [= s & s [= q ) } by Def12;
then ( r in [#p,q#] iff ex s being Element of L st
( r = s & p [= s & s [= q ) ) ;
hence ( r in [#p,q#] iff ( p [= r & r [= q ) ) ; :: thesis: verum