[:n,n:] c= [:n,n:] ;
then reconsider f = [:n,n:] as Relation of n ;
reconsider R = RelStr(# n,(f \ (id n)) #) as NatRelStr of n by Def7;
take R ; :: thesis: the InternalRel of R = [:n,n:] \ (id n)
thus the InternalRel of R = [:n,n:] \ (id n) ; :: thesis: verum