let G be Group; :: thesis: for H being Subgroup of G holds
( H is proper iff the carrier of G \ the carrier of H is non empty set )
let H be Subgroup of G; :: thesis: ( H is proper iff the carrier of G \ the carrier of H is non empty set )
set UG = the carrier of G;
set UH = the carrier of H;
thus ( H is proper implies the carrier of G \ the carrier of H is non empty set ) :: thesis: ( the carrier of G \ the carrier of H is non empty set implies H is proper )

proof

assume A1: H is proper ; :: thesis: the carrier of G \ the carrier of H is non empty set
( the carrier of H c= the carrier of G & the carrier of H <> the carrier of G ) by A1, Th10, GROUP_2:def 5;
then ( ( for x being object st x in the carrier of H holds
x in the carrier of G ) & not for x being object holds
( x in the carrier of H iff x in the carrier of G ) ) by TARSKI:2;
hence the carrier of G \ the carrier of H is non empty set by XBOOLE_0:def 5; :: thesis: verum

end;

thus ( the carrier of G \ the carrier of H is non empty set implies H is proper ) ; :: thesis: verum