[#] R c= UAp ([#] R)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [#] R or y in UAp ([#] R) )
assume A1: y in [#] R ; :: thesis: y in UAp ([#] R)
then Class ( the InternalRel of R,y) meets [#] R by XBOOLE_1:28;
hence y in UAp ([#] R) by A1; :: thesis: verum
end;
hence UAp ([#] R) = [#] R ; :: thesis: verum