let L be Lattice; :: thesis: for q, p being Element of holds
( q in <.p.) iff p [= q )
let q, p be Element of ; :: thesis: ( q in <.p.) iff p [= q )
( q in <.p.) iff ex r being Element of st
( q = r & p [= r ) ) ;
hence ( q in <.p.) iff p [= q ) ; :: thesis: verum