let L be Lattice; :: thesis: for D being non empty Subset of L
for D9 being non empty Subset of (L .: ) holds
( <.(D .: ).) = (.D.> & <.D.) = (.(D .: ).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> )
let D be non empty Subset of L; :: thesis: for D9 being non empty Subset of (L .: ) holds
( <.(D .: ).) = (.D.> & <.D.) = (.(D .: ).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> )
let D9 be non empty Subset of (L .: ); :: thesis: ( <.(D .: ).) = (.D.> & <.D.) = (.(D .: ).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> )
A1: for L being Lattice
for D being non empty Subset of L holds <.(D .: ).) = (.D.>

proof

let L be Lattice; :: thesis: for D being non empty Subset of L holds <.(D .: ).) = (.D.>
let D be non empty Subset of L; :: thesis: <.(D .: ).) = (.D.>
(.D.> .: = (.D.> ;
then A2: ( D c= (.D.> implies <.(D .: ).) c= (.D.> ) by FILTER_0:def 5;
.: <.(D .: ).) = <.(D .: ).) ;
then ( D c= <.(D .: ).) implies (.D.> c= <.(D .: ).) ) by Def11;
hence <.(D .: ).) = (.D.> by A2, Def11, FILTER_0:def 5, XBOOLE_0:def 10; :: thesis: verum

end;

( <.((D .: ) .: ).) = <.D.) & <.(((.: D9) .: ) .: ).) = <.(.: D9).) ) by Lm1;
hence ( <.(D .: ).) = (.D.> & <.D.) = (.(D .: ).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> ) by A1; :: thesis: verum