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)
proof
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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {A} or x in 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