let L1 be Semilattice; :: thesis: for L2 being non empty RelStr
for x, y being Element of L1
for x1, y1 being Element 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 Element of L1
for x1, y1 being Element 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 Element of L1; :: thesis: for x1, y1 being Element 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 Element 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
A3: L2 is with_infima Poset by A1, WAYBEL_8:12, WAYBEL_8:13, WAYBEL_8:14, YELLOW_7:14;
A4: ex_inf_of {x,y},L1 by YELLOW_0:21;
thus x "/\" y = inf {x,y} by YELLOW_0:40
.= inf {x1,y1} by A1, A2, A4, YELLOW_0:27
.= x1 "/\" y1 by A3, YELLOW_0:40 ; :: thesis: verum