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

proof

let L be Lattice; :: thesis: for D being non empty Subset of holds <.(D .: ).) = (.D.>
let D be non empty Subset of ; :: 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.) & <.(((.: D') .: ) .: ).) = <.(.: D').) ) by Lm1;
hence ( <.(D .: ).) = (.D.> & <.D.) = (.(D .: ).> & <.(.: D').) = (.D'.> & <.D'.) = (.(.: D').> ) by A1; :: thesis: verum