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