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