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 4;
.: <.(D .:).) = <.(D .:).) ;
then ( D c= <.(D .:).) implies (.D.> c= <.(D .:).) ) by Def9;
hence <.(D .:).) = (.D.> by A2, Def9, FILTER_0:def 4; :: thesis: verum

end;

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