let L1, L2 be Lattice; 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; 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; ( 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
; ( <.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; XBOOLE_0:def 10 (.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; XBOOLE_0:def 10 verum