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 that
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 #) and
A2: D1 = D2 ; :: thesis: ( <.D1.) = <.D2.) & (.D1.> = (.D2.> )
A3: ( D1 c= <.D1.) & D2 c= <.D2.) ) by FILTER_0:def 4;
( <.D1.) is Filter of L2 & <.D2.) is Filter of L1 ) by A1, Th15;
hence ( <.D1.) c= <.D2.) & <.D2.) c= <.D1.) ) by A2, A3, FILTER_0:def 4; :: according to XBOOLE_0:def 10 :: thesis: (.D1.> = (.D2.>
A4: ( D1 c= (.D1.> & D2 c= (.D2.> ) by Def9;
( (.D1.> is Ideal of L2 & (.D2.> is Ideal of L1 ) by A1, Th16;
hence ( (.D1.> c= (.D2.> & (.D2.> c= (.D1.> ) by A2, A4, Def9; :: according to XBOOLE_0:def 10 :: thesis: verum