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