reconsider B = Left_Cosets H as finite set by A1;
take card B ; :: thesis: ex B being finite set st
( B = Left_Cosets H & card B = card B )
take B ; :: thesis: ( B = Left_Cosets H & card B = card B )
thus ( B = Left_Cosets H & card B = card B ) ; :: thesis: verum