let G be Group; :: thesis: for H1 being Subgroup of G
for H3, H2 being strict Subgroup of G st H1 is Subgroup of H2 holds
H1 "\/" H3 is Subgroup of H2 "\/" H3
let H1 be Subgroup of G; :: thesis: for H3, H2 being strict Subgroup of G st H1 is Subgroup of H2 holds
H1 "\/" H3 is Subgroup of H2 "\/" H3
let H3, H2 be strict Subgroup of G; :: thesis: ( H1 is Subgroup of H2 implies H1 "\/" H3 is Subgroup of H2 "\/" H3 )
assume A1: H1 is Subgroup of H2 ; :: thesis: H1 "\/" H3 is Subgroup of H2 "\/" H3
(H1 "\/" H3) "\/" (H2 "\/" H3) = ((H1 "\/" H3) "\/" H2) "\/" H3 by Th57
.= (H1 "\/" (H3 "\/" H2)) "\/" H3 by Th57
.= (H1 "\/" (H2 "\/" H3)) "\/" H3
.= ((H1 "\/" H2) "\/" H3) "\/" H3 by Th57
.= (H2 "\/" H3) "\/" H3 by A1, Th61
.= H2 "\/" (H3 "\/" H3) by Th57
.= H2 "\/" H3 by Th31 ;
hence H1 "\/" H3 is Subgroup of H2 "\/" H3 by Th61; :: thesis: verum