let L1, L2 be Lattice; :: thesis: for D1 being non empty Subset of L1
for D2 being non empty Subset of L2 st LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) & D1 = D2 holds
( <.D1.) = <.D2.) & (.D1.> = (.D2.> )
let D1 be non empty Subset of L1; :: thesis: for D2 being non empty Subset of L2 st LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) & D1 = D2 holds
( <.D1.) = <.D2.) & (.D1.> = (.D2.> )
let D2 be non empty Subset of L2; :: thesis: ( LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) & D1 = D2 implies ( <.D1.) = <.D2.) & (.D1.> = (.D2.> ) )
assume A1: ( LattStr(# the carrier of L1,the L_join of L1,the L_meet of L1 #) = LattStr(# the carrier of L2,the L_join of L2,the L_meet of L2 #) & D1 = D2 ) ; :: thesis: ( <.D1.) = <.D2.) & (.D1.> = (.D2.> )
then ( D1 c= <.D1.) & ( for I being Filter of L1 st D1 c= I holds
<.D1.) c= I ) & D2 c= <.D2.) & ( for I being Filter of L2 st D2 c= I holds
<.D2.) c= I ) & <.D1.) is Filter of L2 & <.D2.) is Filter of L1 ) by Th16, FILTER_0:def 5;
hence ( <.D1.) c= <.D2.) & <.D2.) c= <.D1.) ) by A1; :: according to XBOOLE_0:def 10 :: thesis: (.D1.> = (.D2.>
( D1 c= (.D1.> & ( for I being Ideal of L1 st D1 c= I holds
(.D1.> c= I ) & D2 c= (.D2.> & ( for I being Ideal of L2 st D2 c= I holds
(.D2.> c= I ) & (.D1.> is Ideal of L2 & (.D2.> is Ideal of L1 ) by A1, Def11, Th17;
hence ( (.D1.> c= (.D2.> & (.D2.> c= (.D1.> ) by A1; :: according to XBOOLE_0:def 10 :: thesis: verum