let L1 be Semilattice; :: thesis: for L2 being non empty RelStr
for X, Y being Subset of L1
for X1, Y1 being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = X1 & Y = Y1 holds
X "/\" Y = X1 "/\" Y1
let L2 be non empty RelStr ; :: thesis: for X, Y being Subset of L1
for X1, Y1 being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = X1 & Y = Y1 holds
X "/\" Y = X1 "/\" Y1
let X, Y be Subset of L1; :: thesis: for X1, Y1 being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = X1 & Y = Y1 holds
X "/\" Y = X1 "/\" Y1
let X1, Y1 be Subset of L2; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = X1 & Y = Y1 implies X "/\" Y = X1 "/\" Y1 )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: ( X = X1 & Y = Y1 ) ; :: thesis: X "/\" Y = X1 "/\" Y1
set XY = { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } ;
set XY1 = { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } ;
A3: { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } = { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) }
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } c= { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) }
let a be object ; :: thesis: ( a in { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } implies a in { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } )
assume a in { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } ; :: thesis: a in { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) }
then consider x, y being Element of L1 such that
A4: a = x "/\" y and
A5: ( x in X & y in Y ) ;
reconsider x1 = x, y1 = y as Element of L2 by A1;
a = x1 "/\" y1 by A1, A4, Th9;
hence a in { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } by A2, A5; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } or a in { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } )
assume a in { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } ; :: thesis: a in { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) }
then consider x, y being Element of L2 such that
A6: a = x "/\" y and
A7: ( x in X1 & y in Y1 ) ;
reconsider x1 = x, y1 = y as Element of L1 by A1;
a = x1 "/\" y1 by A1, A6, Th9;
hence a in { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } by A2, A7; :: thesis: verum
end;
thus X "/\" Y = { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } by YELLOW_4:def 4
.= X1 "/\" Y1 by A3, YELLOW_4:def 4 ; :: thesis: verum