consider T being non empty trivial finite reflexive discrete strict TopRelStr ;
take T ; :: thesis: ( T is strict & T is complete & T is trivial )
thus ( T is strict & T is complete & T is trivial ) ; :: thesis: verum