thus UAp ({} R) c= {} R :: according to XBOOLE_0:def 10 :: thesis: {} R c= UAp ({} R)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in UAp ({} R) or y in {} R )
assume y in UAp ({} R) ; :: thesis: y in {} R
then consider z being Element of R such that
A1: ( y = z & Class ( the InternalRel of R,z) meets {} R ) ;
thus y in {} R by A1; :: thesis: verum
end;
thus {} R c= UAp ({} R) ; :: thesis: verum