thus for G being trivial Group holds
( card G = 1 & G is finite ) :: thesis: for G being Group st card G = 1 holds
G is trivial

proof

let G be trivial Group; :: thesis: ( card G = 1 & G is finite )
ex x being object st the carrier of G = {x} by Def2;
hence ( card G = 1 & G is finite ) by CARD_1:30; :: thesis: verum

end;

let G be Group; :: thesis: ( card G = 1 implies G is trivial )
assume card G = 1 ; :: thesis: G is trivial
hence ex x being object st the carrier of G = {x} by CARD_2:42; :: according to GROUP_6:def 2 :: thesis: verum