let R be non empty RelStr ; :: thesis: for a, b being Element of R st a in UAp {b} holds
[a,b] in the InternalRel of R
let a, b be Element of R; :: thesis: ( a in UAp {b} implies [a,b] in the InternalRel of R )
assume a in UAp {b} ; :: thesis: [a,b] in the InternalRel of R
then consider x being Element of R such that
A1: ( x = a & Class ( the InternalRel of R,x) meets {b} ) ;
consider y being object such that
A2: y in (Class ( the InternalRel of R,x)) /\ {b} by A1, XBOOLE_0:def 1;
( y in Class ( the InternalRel of R,x) & y in {b} ) by XBOOLE_0:def 4, A2;
then ( y = b & y in Class ( the InternalRel of R,x) ) by TARSKI:def 1;
hence [a,b] in the InternalRel of R by A1, RELAT_1:169; :: thesis: verum