let L1, L2 be Lattice; :: thesis: for D1, E1 being non empty Subset of L1
for D2, E2 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 & E1 = E2 holds
D1 "/\" E1 = D2 "/\" E2
let D1, E1 be non empty Subset of L1; :: thesis: for D2, E2 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 & E1 = E2 holds
D1 "/\" E1 = D2 "/\" E2
let D2, E2 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 & E1 = E2 implies D1 "/\" E1 = D2 "/\" E2 )
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 & E1 = E2 ) ; :: thesis: D1 "/\" E1 = D2 "/\" E2
thus D1 "/\" E1 c= D2 "/\" E2 :: according to XBOOLE_0:def 10 :: thesis: D2 "/\" E2 c= D1 "/\" E1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D1 "/\" E1 or x in D2 "/\" E2 )
assume x in D1 "/\" E1 ; :: thesis: x in D2 "/\" E2
then consider a, b being Element of L1 such that
A2: ( x = a "/\" b & a in D1 & b in E1 ) ;
reconsider a' = a, b' = b as Element of L2 by A1;
x = a' "/\" b' by A1, A2;
hence x in D2 "/\" E2 by A1, A2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D2 "/\" E2 or x in D1 "/\" E1 )
assume x in D2 "/\" E2 ; :: thesis: x in D1 "/\" E1
then consider a, b being Element of L2 such that
A3: ( x = a "/\" b & a in D2 & b in E2 ) ;
reconsider a' = a, b' = b as Element of L1 by A1;
x = a' "/\" b' by A1, A3;
hence x in D1 "/\" E1 by A1, A3; :: thesis: verum