let G be Group; :: thesis: for N, H being Subgroup of G holds N ` H c= carr H

let N, H be Subgroup of G; :: thesis: N ` H c= carr H

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N ` H or x in carr H )

assume x in N ` H ; :: thesis: x in carr H

then consider y1 being Element of G such that

A1: ( y1 = x & y1 * N c= carr H ) ;

y1 in y1 * N by GROUP_2:108;

hence x in carr H by A1; :: thesis: verum

let N, H be Subgroup of G; :: thesis: N ` H c= carr H

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N ` H or x in carr H )

assume x in N ` H ; :: thesis: x in carr H

then consider y1 being Element of G such that

A1: ( y1 = x & y1 * N c= carr H ) ;

y1 in y1 * N by GROUP_2:108;

hence x in carr H by A1; :: thesis: verum