let O be set ; :: thesis: for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds
( H1 is StableSubgroup of H1 "\/" H2 & H2 is StableSubgroup of H1 "\/" H2 )
let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G holds
( H1 is StableSubgroup of H1 "\/" H2 & H2 is StableSubgroup of H1 "\/" H2 )
let H1, H2 be StableSubgroup of G; :: thesis: ( H1 is StableSubgroup of H1 "\/" H2 & H2 is StableSubgroup of H1 "\/" H2 )
H1 "\/" H2 = H2 "\/" H1 ;
hence ( H1 is StableSubgroup of H1 "\/" H2 & H2 is StableSubgroup of H1 "\/" H2 ) by Lm32; :: thesis: verum