let L be Lattice; :: thesis: for D1, D2 being non empty Subset of L st D1 c= D2 holds
<.D1.) c= <.D2.)
let D1, D2 be non empty Subset of L; :: thesis: ( D1 c= D2 implies <.D1.) c= <.D2.) )
assume A1: D1 c= D2 ; :: thesis: <.D1.) c= <.D2.)
D2 c= <.D2.) by Def4;
then D1 c= <.D2.) by A1;
hence <.D1.) c= <.D2.) by Def4; :: thesis: verum