let L1, L2 be non empty RelStr ; :: thesis: ( L1,L2 are_isomorphic implies card the carrier of L1 = card the carrier of L2 )
assume L1,L2 are_isomorphic ; :: thesis: card the carrier of L1 = card the carrier of L2
then consider f being Function of L1,L2 such that
A1: f is isomorphic by WAYBEL_1:def 8;
A2: dom f = the carrier of L1 by FUNCT_2:def 1;
( f is one-to-one & rng f = the carrier of L2 ) by A1, WAYBEL_0:66;
then the carrier of L1, the carrier of L2 are_equipotent by A2, WELLORD2:def 4;
hence card the carrier of L1 = card the carrier of L2 by CARD_1:5; :: thesis: verum