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 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 & 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 object ; :: 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
A3: x = a "/\" b and
A4: ( a in D1 & b in E1 ) ;
reconsider a9 = a, b9 = b as Element of L2 by A1;
x = a9 "/\" b9 by A1, A3;
hence x in D2 "/\" E2 by A2, A4; :: thesis: verum

end;

let x be object ; :: 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
A5: x = a "/\" b and
A6: ( a in D2 & b in E2 ) ;
reconsider a9 = a, b9 = b as Element of L1 by A1;
x = a9 "/\" b9 by A1, A5;
hence x in D1 "/\" E1 by A2, A6; :: thesis: verum