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 Th75
.= (H1 "\/" (H3 "\/" H2)) "\/" H3 by Th75
.= (H1 "\/" (H2 "\/" H3)) "\/" H3
.= ((H1 "\/" H2) "\/" H3) "\/" H3 by Th75
.= (H2 "\/" H3) "\/" H3 by A1, Th79
.= H2 "\/" (H3 "\/" H3) by Th75
.= H2 "\/" H3 by Th40 ;
hence H1 "\/" H3 is Subgroup of H2 "\/" H3 by Th79; :: thesis: verum