set R = the total reflexive symmetric transitive Relation of U;
take the total reflexive symmetric transitive Relation of U ; :: thesis: the total reflexive symmetric transitive Relation of U is total
thus the total reflexive symmetric transitive Relation of U is total ; :: thesis: verum