consider x, y being Element of A such that
A1: ( x <> y & [x,y] in the InternalRel of A ) by Th4;
set X = {x};
A2: x in {x} by TARSKI:def 1;
{x} c= UAp {x} by Th13;
then y in UAp {x} by A1, A2, Th37;
then UAp {x} <> {x} by A1, TARSKI:def 1;
then {x} is rough by Th16;
hence ex b₁ being Subset of A st b₁ is rough ; :: thesis: verum