let L be Lattice; :: thesis: for p being Element of L holds
( (.p.> = <.(p .: ).) & (.(p .: ).> = <.p.) )
let p be Element of L; :: thesis: ( (.p.> = <.(p .: ).) & (.(p .: ).> = <.p.) )
(.p.> = .: <.(p .: ).)

proof

let q be Element of L; :: according to FILTER_2:def 1 :: thesis: ( q in (.p.> iff q in .: <.(p .: ).) )
( ( q in (.p.> implies q [= p ) & ( q [= p implies q in (.p.> ) & ( q .: in <.(p .: ).) implies p .: [= q .: ) & ( p .: [= q .: implies q .: in <.(p .: ).) ) & ( p .: [= q .: implies q [= p ) & ( q [= p implies p .: [= q .: ) & p .: = p & q .: = q & .: <.(p .: ).) = <.(p .: ).) ) by Th29, FILTER_0:18, LATTICE2:53, LATTICE2:54;
hence ( q in (.p.> iff q in .: <.(p .: ).) ) ; :: thesis: verum

end;

hence (.p.> = <.(p .: ).) ; :: thesis: (.(p .: ).> = <.p.)
.: (.(p .: ).> = <.p.)

proof

let q be Element of L; :: according to FILTER_2:def 1 :: thesis: ( q in .: (.(p .: ).> iff q in <.p.) )
( ( q .: in (.(p .: ).> implies q .: [= p .: ) & ( q .: [= p .: implies q .: in (.(p .: ).> ) & ( q in <.p.) implies p [= q ) & ( p [= q implies q in <.p.) ) & ( p [= q implies q .: [= p .: ) & ( q .: [= p .: implies p [= q ) & p .: = p & q .: = q & .: (.(p .: ).> = (.(p .: ).> ) by Th29, FILTER_0:18, LATTICE2:53, LATTICE2:54;
hence ( q in .: (.(p .: ).> iff q in <.p.) ) ; :: thesis: verum

end;

hence (.(p .: ).> = <.p.) ; :: thesis: verum