{ x where x is Element of R : Class ( the InternalRel of R,x) c= [#] R } = [#] R

proof

thus { x where x is Element of R : Class ( the InternalRel of R,x) c= [#] R } c= [#] R :: according to XBOOLE_0:def 10 :: thesis: [#] R c= { x where x is Element of R : Class ( the InternalRel of R,x) c= [#] R }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of R : Class ( the InternalRel of R,x) c= [#] R } or y in [#] R )
assume y in { x where x is Element of R : Class ( the InternalRel of R,x) c= [#] R } ; :: thesis: y in [#] R
then ex z being Element of R st
( z = y & Class ( the InternalRel of R,z) c= [#] R ) ;
hence y in [#] R ; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [#] R or y in { x where x is Element of R : Class ( the InternalRel of R,x) c= [#] R } )
assume A1: y in [#] R ; :: thesis: y in { x where x is Element of R : Class ( the InternalRel of R,x) c= [#] R }
assume not y in { x where x is Element of R : Class ( the InternalRel of R,x) c= [#] R } ; :: thesis: contradiction
then ( not y is Element of R or not Class ( the InternalRel of R,y) c= [#] R ) ;
hence contradiction by A1; :: thesis: verum

end;

hence LAp ([#] R) = [#] R ; :: thesis: verum