let L1 be sup-Semilattice; 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 ; 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; 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; ( 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 )
; 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
; verum