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