let A be non degenerated commutative Ring; :: thesis: for J being proper Ideal of A holds multClSet (J,(1. A)) = {(1. A)}
let J be proper Ideal of A; :: thesis: multClSet (J,(1. A)) = {(1. A)}
thus multClSet (J,(1. A)) c= {(1. A)} :: according to XBOOLE_0:def 10 :: thesis: {(1. A)} c= multClSet (J,(1. A))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in multClSet (J,(1. A)) or x in {(1. A)} )
assume x in multClSet (J,(1. A)) ; :: thesis: x in {(1. A)}
then consider n1 being Nat such that
A3: x = (1. A) |^ n1 ;
x = 1. A by A3, Lm4;
hence x in {(1. A)} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(1. A)} or x in multClSet (J,(1. A)) )
assume x in {(1. A)} ; :: thesis: x in multClSet (J,(1. A))
then x = 1. A by TARSKI:def 1;
hence x in multClSet (J,(1. A)) by C0SP1:def 4; :: thesis: verum