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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in Inter A,A or x in {A} )
assume x in Inter A,A ; :: thesis: x in {A}
then ( A c= x & x c= A ) by Lemacik;
then A = x by XBOOLE_0:def 10;
hence x in {A} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: 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