let R be non empty RelStr ; for a, b being Element of R st [a,b] in the InternalRel of R holds
a in UAp {b}
let a, b be Element of R; ( [a,b] in the InternalRel of R implies a in UAp {b} )
B1:
b in {b}
by TARSKI:def 1;
assume
[a,b] in the InternalRel of R
; a in UAp {b}
then B3:
b in Class ( the InternalRel of R,a)
by RELAT_1:169;
reconsider B = {b} as Subset of R ;
B2:
Class ( the InternalRel of R,a) meets B
by B3, B1, XBOOLE_0:3;
UAp B = { x where x is Element of R : Class ( the InternalRel of R,x) meets B }
by ROUGHS_1:def 5;
hence
a in UAp {b}
by B2; verum