let x be object ; :: thesis: product <*{x}*> = {<*x*>}
{ <*y*> where y is Element of {x} : verum } = {<*x*>}

proof

set SA = { <*y*> where y is Element of {x} : verum } ;
A1: for t being object st t in { <*y*> where y is Element of {x} : verum } holds
t in {<*x*>}

proof

let t be object ; :: thesis: ( t in { <*y*> where y is Element of {x} : verum } implies t in {<*x*>} )
assume t in { <*y*> where y is Element of {x} : verum } ; :: thesis: t in {<*x*>}
then consider y0 being Element of {x} such that
A2: t = <*y0*> ;
t = <*x*> by A2, TARSKI:def 1;
hence t in {<*x*>} by TARSKI:def 1; :: thesis: verum

end;

for t being object st t in {<*x*>} holds
t in { <*y*> where y is Element of {x} : verum }

proof

let t be object ; :: thesis: ( t in {<*x*>} implies t in { <*y*> where y is Element of {x} : verum } )
assume t in {<*x*>} ; :: thesis: t in { <*y*> where y is Element of {x} : verum }
then ( t = <*x*> & x is Element of {x} ) by TARSKI:def 1;
hence t in { <*y*> where y is Element of {x} : verum } ; :: thesis: verum

end;

then ( { <*y*> where y is Element of {x} : verum } c= {<*x*>} & {<*x*>} c= { <*y*> where y is Element of {x} : verum } ) by A1;
hence { <*y*> where y is Element of {x} : verum } = {<*x*>} ; :: thesis: verum

end;

hence product <*{x}*> = {<*x*>} by SRINGS_4:24; :: thesis: verum