let R be non empty RelStr ; 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; ( a in UAp {b} implies [a,b] in the InternalRel of R )
assume
a in UAp {b}
; [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; verum