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