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 Th25;

now

let a be Element of H; :: thesis: a * a = a
reconsider a9 = a as Element of G by A2, TARSKI:def 3;
thus a * a = a9 * a9 by Th27
.= a by A1, Th9 ; :: thesis: verum

end;

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