take the finite 1 -element reflexive discrete strict TopRelStr ; :: thesis: ( the finite 1 -element reflexive discrete strict TopRelStr is strict & the finite 1 -element reflexive discrete strict TopRelStr is complete & the finite 1 -element reflexive discrete strict TopRelStr is 1 -element )
thus ( the finite 1 -element reflexive discrete strict TopRelStr is strict & the finite 1 -element reflexive discrete strict TopRelStr is complete & the finite 1 -element reflexive discrete strict TopRelStr is 1 -element ) ; :: thesis: verum