{ x where x is Element of R : Class ( the InternalRel of R,x) c= {} R } 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 consider z being Element of R such that
A1: ( z = y & Class ( the InternalRel of R,z) c= {} R ) ;
thus y in {} R by A1; :: thesis: verum
end;
hence LAp ({} R) = {} R ; :: thesis: verum