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