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