let U be Universe; :: thesis: for x being set holds
( x is U -petit iff card x in card U )
let x be set ; :: thesis: ( x is U -petit iff card x in card U )

hereby :: thesis: ( card x in card U implies x is U -petit )

assume x is U -petit ; :: thesis: card x in card U
then consider u being Element of U such that
A1: u,x are_equipotent ;
card u = card x by A1, CARD_1:5;
hence card x in card U by CLASSES4:30; :: thesis: verum

end;

assume card x in card U ; :: thesis: x is U -petit
then reconsider u = card x as Element of U by CLASSES2:13;
card u = card x ;
hence x is U -petit by CARD_1:5; :: thesis: verum