let R be non empty reflexive RelStr ; :: thesis: for X being Subset of R holds X c= UAp X
let X be Subset of R; :: thesis: X c= UAp X
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in UAp X )
assume A1: y in X ; :: thesis: y in UAp X
then y in Class ( the InternalRel of R,y) by Th4;
then Class ( the InternalRel of R,y) meets X by A1, XBOOLE_0:def 4;
hence y in UAp X by A1; :: thesis: verum