let L be Lattice; :: thesis: for D being non empty Subset of L
for D' being non empty Subset of (L .: ) holds
( <.(D .: ).) = (.D.> & <.D.) = (.(D .: ).> & <.(.: D').) = (.D'.> & <.D'.) = (.(.: D').> )
let D be non empty Subset of L; :: thesis: for D' being non empty Subset of (L .: ) holds
( <.(D .: ).) = (.D.> & <.D.) = (.(D .: ).> & <.(.: D').) = (.D'.> & <.D'.) = (.(.: D').> )
let D' be non empty Subset of (L .: ); :: thesis: ( <.(D .: ).) = (.D.> & <.D.) = (.(D .: ).> & <.(.: D').) = (.D'.> & <.D'.) = (.(.: D').> )
A1: ( <.((D .: ) .: ).) = <.D.) & <.(((.: D') .: ) .: ).) = <.(.: D').) & (.((.: D') .: ).> = (.D'.> ) by Lm1;
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 & (.D.> .: = (.D.> & .: <.(D .: ).) = <.(D .: ).) ) ;
then ( D c= (.D.> & ( D c= <.(D .: ).) implies (.D.> c= <.(D .: ).) ) & D c= <.(D .: ).) & ( D c= (.D.> implies <.(D .: ).) c= (.D.> ) ) by Def11, FILTER_0:def 5;
hence <.(D .: ).) = (.D.> by XBOOLE_0:def 10; :: thesis: verum

end;

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