let R be non empty RelStr ; :: thesis: for X being Subset of R holds Uap X = UAp X
let X be Subset of R; :: thesis: Uap X = UAp X
A1: LAp (X `) misses UAp X
proof
assume LAp (X `) meets UAp X ; :: thesis: contradiction
then consider x being object such that
A2: ( x in LAp (X `) & x in UAp X ) by XBOOLE_0:3;
( Class ( the InternalRel of R,x) meets X & Class ( the InternalRel of R,x) c= X ` ) by A2, Th6, Th7;
hence contradiction by XBOOLE_1:63, XBOOLE_1:79; :: thesis: verum
end;
(UAp X) ` c= LAp (X `)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (UAp X) ` or x in LAp (X `) )
assume A3: x in (UAp X) ` ; :: thesis: x in LAp (X `)
then not x in UAp X by XBOOLE_0:def 5;
then Class ( the InternalRel of R,x) misses X by A3;
then Class ( the InternalRel of R,x) c= X ` by SUBSET_1:23;
hence x in LAp (X `) by A3; :: thesis: verum
end;
hence Uap X = UAp X by A1, SUBSET_1:17, SUBSET_1:23; :: thesis: verum