let L1, L2 be non empty up-complete Poset; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies Sigma L1 = Sigma L2 )
assume RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: Sigma L1 = Sigma L2
then A1: RelStr(# the carrier of (Sigma L2), the InternalRel of (Sigma L2) #) = RelStr(# the carrier of L1, the InternalRel of L1 #) by YELLOW_9:def 4;
then ( RelStr(# the carrier of (Sigma L1), the InternalRel of (Sigma L1) #) = RelStr(# the carrier of L1, the InternalRel of L1 #) & Sigma L2 is TopAugmentation of L1 ) by YELLOW_9:def 4;
hence Sigma L1 = Sigma L2 by A1, Th13; :: thesis: verum