let L be Lattice; :: thesis: for D, D1, D2 being non empty Subset of L holds
( ( D1 c= D2 implies (.D1.> c= (.D2.> ) & (.(.D.>.> c= (.D.> )
let D, D1, D2 be non empty Subset of L; :: thesis: ( ( D1 c= D2 implies (.D1.> c= (.D2.> ) & (.(.D.>.> c= (.D.> )
D2 c= (.D2.> by Def9;
then ( D1 c= D2 implies D1 c= (.D2.> ) ;
hence ( ( D1 c= D2 implies (.D1.> c= (.D2.> ) & (.(.D.>.> c= (.D.> ) by Def9; :: thesis: verum