let L1 be sup-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_suprema Poset by A1, WAYBEL_8:12, WAYBEL_8:13, WAYBEL_8:14, YELLOW_7:15;
A4: ex_sup_of {x,y},L1 by YELLOW_0:20;
thus x "\/" y = sup {x,y} by YELLOW_0:41
.= sup {x1,y1} by A1, A2, A4, YELLOW_0:26
.= x1 "\/" y1 by A3, YELLOW_0:41 ; :: thesis: verum