let M be non empty multMagma ; :: thesis: for A being Subset of M holds
( A is stable iff A * A c= A )
let A be Subset of M; :: thesis: ( A is stable iff A * A c= A )

hereby :: thesis: ( A * A c= A implies A is stable )

assume A1: A is stable ; :: thesis: A * A c= A
for x being object st x in A * A holds
x in A

proof

let x be object ; :: thesis: ( x in A * A implies x in A )
assume x in A * A ; :: thesis: x in A
then consider v, w being Element of M such that
A2: ( x = v * w & v in A & w in A ) by GROUP_2:8;
thus x in A by A1, A2; :: thesis: verum

end;

hence A * A c= A ; :: thesis: verum

end;

assume A3: A * A c= A ; :: thesis: A is stable
for v, w being Element of M st v in A & w in A holds
v * w in A

proof

let v, w be Element of M; :: thesis: ( v in A & w in A implies v * w in A )
assume ( v in A & w in A ) ; :: thesis: v * w in A
then v * w in A * A by GROUP_2:8;
hence v * w in A by A3; :: thesis: verum

end;

hence A is stable ; :: thesis: verum