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 .: ).) )
A1: ( q .: in <.(p .: ).) iff p .: [= q .: ) by FILTER_0:18;
( q in (.p.> iff q [= p ) by Th29;
hence ( q in (.p.> iff q in .: <.(p .: ).) ) by A1, LATTICE2:53, LATTICE2:54; :: 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.) )
A2: ( q in <.p.) iff p [= q ) by FILTER_0:18;
( q .: in (.(p .: ).> iff q .: [= p .: ) by Th29;
hence ( q in .: (.(p .: ).> iff q in <.p.) ) by A2, LATTICE2:53, LATTICE2:54; :: thesis: verum

end;

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