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

LAp X = LAp 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

LAp X = LAp 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 LAp X = LAp 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: LAp X = LAp Y

LAp X = { x where x is Element of R1 : Class ( the InternalRel of R1,x) c= X } by ROUGHS_1:def 4

.= LAp Y by A1, A2, ROUGHS_1:def 4 ;

hence LAp X = LAp 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

LAp X = LAp 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

LAp X = LAp 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 LAp X = LAp 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: LAp X = LAp Y

LAp X = { x where x is Element of R1 : Class ( the InternalRel of R1,x) c= X } by ROUGHS_1:def 4

.= LAp Y by A1, A2, ROUGHS_1:def 4 ;

hence LAp X = LAp Y ; :: thesis: verum