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
LAp T = LAp 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 LAp T = LAp R )
assume A0: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) ; :: thesis: LAp T = LAp R
for x being Element of bool the carrier of R holds (LAp T) . x = (LAp R) . x

proof

let x be Element of bool the carrier of R; :: thesis: (LAp T) . x = (LAp R) . x
reconsider xx = x as Subset of R ;
A2: (LAp R) . xx = LAp xx by ROUGHS_2:def 10;
reconsider y = x as Subset of T by A0;
(LAp T) . y = LAp y by ROUGHS_2:def 10;
hence (LAp T) . x = (LAp R) . x by A2, A0; :: thesis: verum

end;

hence LAp T = LAp R by A0; :: thesis: verum