let T be non empty TopRelStr ; :: thesis: for R being non empty RelStr st RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) holds
UAp T = UAp R
let R be non empty RelStr ; :: thesis: ( RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) implies UAp T = UAp R )
assume A0: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) ; :: thesis: UAp T = UAp R
for x being Element of bool the carrier of R holds (UAp T) . x = (UAp R) . x
proof
let x be Element of bool the carrier of R; :: thesis: (UAp T) . x = (UAp R) . x
reconsider xx = x as Subset of R ;
A2: (UAp R) . xx = UAp xx by ROUGHS_2:def 11;
reconsider y = x as Subset of T by A0;
(UAp T) . y = UAp y by ROUGHS_2:def 11;
hence (UAp T) . x = (UAp R) . x by A2, A0; :: thesis: verum
end;
hence UAp T = UAp R by A0; :: thesis: verum