let A be Tolerance_Space; :: thesis: for X being Subset of A holds BndAp X = BndAp (X `)
let X be Subset of A; :: thesis: BndAp X = BndAp (X `)
thus BndAp X c= BndAp (X `) :: according to XBOOLE_0:def 10 :: thesis: BndAp (X `) c= BndAp X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in BndAp X or x in BndAp (X `) )
assume A1: x in BndAp X ; :: thesis: x in BndAp (X `)
then x in UAp X by XBOOLE_0:def 5;
then not x in (UAp X) ` by XBOOLE_0:def 5;
then A2: not x in LAp (X `) by Th28;
not x in LAp X by A1, XBOOLE_0:def 5;
then x in (LAp X) ` by A1, XBOOLE_0:def 5;
then x in UAp (X `) by Th29;
hence x in BndAp (X `) by A2, XBOOLE_0:def 5; :: thesis: verum

end;

thus BndAp (X `) c= BndAp X :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in BndAp (X `) or x in BndAp X )
assume A3: x in BndAp (X `) ; :: thesis: x in BndAp X
then x in UAp (X `) by XBOOLE_0:def 5;
then x in (LAp X) ` by Th29;
then A4: not x in LAp X by XBOOLE_0:def 5;
not x in LAp (X `) by A3, XBOOLE_0:def 5;
then not x in (UAp X) ` by Th28;
then x in ((UAp X) `) ` by A3, SUBSET_1:29;
hence x in BndAp X by A4, XBOOLE_0:def 5; :: thesis: verum

end;