let R be non empty RelStr ; :: thesis: for X being Subset of R holds LAp (X `) = (UAp X) `
let X be Subset of R; :: thesis: LAp (X `) = (UAp X) `
thus LAp (X `) c= (UAp X) ` :: according to XBOOLE_0:def 10 :: thesis: (UAp X) ` c= LAp (X `)

proof

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 ` ) ;
not z in { x where x is Element of R : Class ( the InternalRel of R,x) meets X }

proof

assume z in { x where x is Element of R : Class ( the InternalRel of R,x) meets X } ; :: thesis: contradiction
then consider t being Element of R such that
A2: ( t = z & Class ( the InternalRel of R,t) meets X ) ;
thus contradiction by A1, SUBSET_1:23, A2; :: thesis: verum

end;

hence y in (UAp X) ` by A1, XBOOLE_0:def 5; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (UAp X) ` or y in LAp (X `) )
assume A3: y in (UAp X) ` ; :: thesis: y in LAp (X `)
( y in [#] R & not y in UAp X ) by XBOOLE_0:def 5, A3;
then not Class ( the InternalRel of R,y) meets X ;
then Class ( the InternalRel of R,y) c= X ` by SUBSET_1:23;
hence y in LAp (X `) by A3; :: thesis: verum