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 ;
per cases ( ( not S is empty & not R is empty ) or ( S is empty & R is empty ) ) by A2, WAYBEL_0:def 38;
suppose ( not S is empty & not R is empty ) ; :: thesis: card the InternalRel of S = card the InternalRel of R
hence card the InternalRel of S = card the InternalRel of R by A1, Lm1; :: thesis: verum
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;
end;