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:15;
( q in (.p.> iff q [= p ) by Th28;
hence ( q in (.p.> iff q in .: <.(p .:).) ) by A1, LATTICE2:38, LATTICE2:39; :: 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:15;
( q .: in (.(p .:).> iff q .: [= p .: ) by Th28;
hence ( q in .: (.(p .:).> iff q in <.p.) ) by A2, LATTICE2:38, LATTICE2:39; :: thesis: verum

end;

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