let L be Lattice; :: thesis: for D1, D2 being non empty Subset of L holds
( <.(D1 \/ D2).) = <.(<.D1.) \/ D2).) & <.(D1 \/ D2).) = <.(D1 \/ <.D2.)).) )
let D1, D2 be non empty Subset of L; :: thesis: ( <.(D1 \/ D2).) = <.(<.D1.) \/ D2).) & <.(D1 \/ D2).) = <.(D1 \/ <.D2.)).) )

now :: thesis: for D1, D2 being non empty Subset of L holds
( <.(D1 \/ D2).) c= <.(<.D1.) \/ D2).) & <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).) )

let D1, D2 be non empty Subset of L; :: thesis: ( <.(D1 \/ D2).) c= <.(<.D1.) \/ D2).) & <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).) )
( D2 c= D1 \/ D2 & D1 \/ D2 c= <.(D1 \/ D2).) ) by Def4, XBOOLE_1:7;
then A1: D2 c= <.(D1 \/ D2).) ;
D1 c= <.D1.) by Def4;
then D1 \/ D2 c= <.D1.) \/ D2 by XBOOLE_1:9;
hence <.(D1 \/ D2).) c= <.(<.D1.) \/ D2).) by Th22; :: thesis: <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).)
<.D1.) c= <.(D1 \/ D2).) by Th22, XBOOLE_1:7;
then <.D1.) \/ D2 c= <.(D1 \/ D2).) by A1, XBOOLE_1:8;
hence <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).) by Def4; :: thesis: verum

end;

hence ( <.(D1 \/ D2).) c= <.(<.D1.) \/ D2).) & <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).) & <.(D1 \/ D2).) c= <.(D1 \/ <.D2.)).) & <.(D1 \/ <.D2.)).) c= <.(D1 \/ D2).) ) ; :: according to XBOOLE_0:def 10 :: thesis: verum