let S, R be RelStr ; :: thesis: ( S,R are_isomorphic implies card the InternalRel of S = card the InternalRel of R )

assume A1: S,R are_isomorphic ; :: thesis: card the InternalRel of S = card the InternalRel of R

then A2: ex f being Function of S,R st f is isomorphic ;

assume A1: S,R are_isomorphic ; :: thesis: card the InternalRel of S = card the InternalRel of R

then A2: ex f being Function of S,R st f is isomorphic ;

per cases
( ( not S is empty & not R is empty ) or ( S is empty & R is empty ) )
by A2, WAYBEL_0:def 38;

end;

suppose
( not S is empty & not R is empty )
; :: thesis: card the InternalRel of S = card the InternalRel of R

end;

end;

suppose
( S is empty & R is empty )
; :: thesis: card the InternalRel of S = card the InternalRel of R

then reconsider S = S, R = R as empty RelStr ;

( the InternalRel of S = {} & the InternalRel of R = {} ) ;

hence card the InternalRel of S = card the InternalRel of R ; :: thesis: verum

end;( the InternalRel of S = {} & the InternalRel of R = {} ) ;

hence card the InternalRel of S = card the InternalRel of R ; :: thesis: verum