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
then A2: ( H₁(H) c= H₁(G) & ( for a being Element of G holds a * a = a ) ) by Th9, Th25;

now

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

end;

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