let R be non empty RelStr ; :: thesis: for X, Y being Subset of R st X c= Y holds
UAp X c= UAp Y
let X, Y be Subset of R; :: thesis: ( X c= Y implies UAp X c= UAp Y )
assume A1: X c= Y ; :: thesis: UAp X c= UAp Y
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in UAp X or y in UAp Y )
assume y in UAp X ; :: thesis: y in UAp Y
then consider z being Element of R such that
A2: ( z = y & Class ( the InternalRel of R,z) meets X ) ;
Class ( the InternalRel of R,z) meets Y by A1, A2, XBOOLE_1:63;
hence y in UAp Y by A2; :: thesis: verum