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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in BndAp X or x in BndAp (X ` ) )
assume x in BndAp X ; :: thesis: x in BndAp (X ` )
then A1: ( x in UAp X & not x in LAp X ) by XBOOLE_0:def 5;
then x in (LAp X) ` by SUBSET_1:50;
then A2: x in UAp (X ` ) by Th29;
not x in (UAp X) ` by A1, XBOOLE_0:def 5;
then not x in LAp (X ` ) by Th28;
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 set ; :: 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 A4: ( x in UAp (X ` ) & not x in LAp (X ` ) ) by XBOOLE_0:def 5;
then x in (LAp X) ` by Th29;
then A5: not x in LAp X by XBOOLE_0:def 5;
not x in (UAp X) ` by A4, Th28;
then x in ((UAp X) ` ) ` by A3, SUBSET_1:50;
hence x in BndAp X by A5, XBOOLE_0:def 5; :: thesis: verum

end;