let R be non empty void RelStr ; :: thesis: for X being Subset of R holds UAp X = {} R
let X be Subset of R; :: thesis: UAp X = {} R
A1: the InternalRel of R = {} by YELLOW_3:def 3;
{ x where x is Element of R : Class ({},x) meets X } = { x where x is Element of R : {} meets X }

proof

thus { x where x is Element of R : Class ({},x) meets X } c= { x where x is Element of R : {} meets X } :: according to XBOOLE_0:def 10 :: thesis: { x where x is Element of R : {} meets X } c= { x where x is Element of R : Class ({},x) meets X }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of R : Class ({},x) meets X } or y in { x where x is Element of R : {} meets X } )
assume y in { x where x is Element of R : Class ({},x) meets X } ; :: thesis: y in { x where x is Element of R : {} meets X }
then consider z being Element of R such that
A2: ( z = y & Class ({},z) meets X ) ;
thus y in { x where x is Element of R : {} meets X } by A2; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of R : {} meets X } or y in { x where x is Element of R : Class ({},x) meets X } )
assume y in { x where x is Element of R : {} meets X } ; :: thesis: y in { x where x is Element of R : Class ({},x) meets X }
then consider z being Element of R such that
A3: ( z = y & {} meets X ) ;
thus y in { x where x is Element of R : Class ({},x) meets X } by A3; :: thesis: verum

end;

hence UAp X = {} R by Th3, A1; :: thesis: verum