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

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