let U be set ; :: thesis: for A being Subset of U holds Inter (A,A) = {A}

let A be Subset of U; :: thesis: Inter (A,A) = {A}

thus Inter (A,A) c= {A} :: according to XBOOLE_0:def 10 :: thesis: {A} c= Inter (A,A)

assume x in {A} ; :: thesis: x in Inter (A,A)

then x = A by TARSKI:def 1;

hence x in Inter (A,A) ; :: thesis: verum

let A be Subset of U; :: thesis: Inter (A,A) = {A}

thus Inter (A,A) c= {A} :: according to XBOOLE_0:def 10 :: thesis: {A} c= Inter (A,A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {A} or x in Inter (A,A) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Inter (A,A) or x in {A} )

reconsider xx = x as set by TARSKI:1;

assume x in Inter (A,A) ; :: thesis: x in {A}

then ( A c= xx & xx c= A ) by Th1;

then A = x by XBOOLE_0:def 10;

hence x in {A} by TARSKI:def 1; :: thesis: verum

end;reconsider xx = x as set by TARSKI:1;

assume x in Inter (A,A) ; :: thesis: x in {A}

then ( A c= xx & xx c= A ) by Th1;

then A = x by XBOOLE_0:def 10;

hence x in {A} by TARSKI:def 1; :: thesis: verum

assume x in {A} ; :: thesis: x in Inter (A,A)

then x = A by TARSKI:def 1;

hence x in Inter (A,A) ; :: thesis: verum