let R be non empty RelStr ; :: thesis: 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; :: thesis: ( [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 ; :: thesis: 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; :: thesis: verum

a in UAp {b}

let a, b be Element of R; :: thesis: ( [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 ; :: thesis: 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; :: thesis: verum