let L1, L2 be Lattice; :: thesis: for D1, E1 being non empty Subset of
for D2, E2 being non empty Subset of 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 ; :: thesis: for D2, E2 being non empty Subset of 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 ; :: 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 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 such that
A3: x = a "/\" b and
A4: ( a in D1 & b in E1 ) ;
reconsider a' = a, b' = b as Element of by A1;
x = a' "/\" b' by A1, A3;
hence x in D2 "/\" E2 by A2, A4; :: 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 such that
A5: x = a "/\" b and
A6: ( a in D2 & b in E2 ) ;
reconsider a' = a, b' = b as Element of by A1;
x = a' "/\" b' by A1, A5;
hence x in D1 "/\" E1 by A2, A6; :: thesis: verum