let G be non empty multMagma ; :: thesis: for H being non empty SubStr of G st G is idempotent holds
H is idempotent
let H be non empty SubStr of G; :: thesis: ( G is idempotent implies H is idempotent )
assume A1: G is idempotent ; :: thesis: H is idempotent
A2: H₁(H) c= H₁(G) by Th23;

now :: thesis: for a being Element of H holds a * a = a

let a be Element of H; :: thesis: a * a = a
reconsider a9 = a as Element of G by A2;
thus a * a = a9 * a9 by Th25
.= a by A1, Th7 ; :: thesis: verum

end;

hence H is idempotent by Th7; :: thesis: verum