consider A being non empty set ;
reconsider R = id A as Relation of A ;
reconsider R = R as Order of A ;
take RelStr(# A,R #) ; :: thesis: ( RelStr(# A,R #) is strict & RelStr(# A,R #) is discrete & not RelStr(# A,R #) is empty )
thus ( RelStr(# A,R #) is strict & RelStr(# A,R #) is discrete & not RelStr(# A,R #) is empty ) by Def1; :: thesis: verum