let X be set ; :: thesis: for R being total transitive Relation of X holds rho R is axiom_UP3
let R be total transitive Relation of X; :: thesis: rho R is axiom_UP3
let B1 be Element of rho R; :: according to UNIFORM2:def 17 :: thesis: ex b₁ being Element of rho R st b₁ [*] b₁ c= B1
B1 in rho R ;
then consider C being Subset of [:X,X:] such that
A1: B1 = C and
A2: R c= C ;
R in rho R ;
then reconsider B2 = R as Element of rho R ;
R * R c= R by RELAT_2:27;
then B2 * B2 c= B1 by A1, A2;
hence ex B2 being Element of rho R st B2 * B2 c= B1 ; :: thesis: verum