set R = the non empty reflexive transitive RelStr ;
take the non empty reflexive transitive RelStr ; :: thesis: ( not the non empty reflexive transitive RelStr is empty & the non empty reflexive transitive RelStr is mediate & the non empty reflexive transitive RelStr is transitive )
thus ( not the non empty reflexive transitive RelStr is empty & the non empty reflexive transitive RelStr is mediate & the non empty reflexive transitive RelStr is transitive ) ; :: thesis: verum