let R1, R2 be non empty RelStr ; :: thesis: for X being Subset of R1
for Y being Subset of R2 st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & X = Y holds
UAp X = UAp Y
let X be Subset of R1; :: thesis: for Y being Subset of R2 st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & X = Y holds
UAp X = UAp Y
let Y be Subset of R2; :: thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & X = Y implies UAp X = UAp Y )
assume that
A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) and
A2: X = Y ; :: thesis: UAp X = UAp Y
UAp X = { x where x is Element of R1 : Class ( the InternalRel of R1,x) meets X } by ROUGHS_1:def 5
.= UAp Y by A1, A2, ROUGHS_1:def 5 ;
hence UAp X = UAp Y ; :: thesis: verum