let X be set ; :: thesis: for R being symmetric Relation of X holds rho R is axiom_UP2
let R be symmetric Relation of X; :: thesis: rho R is axiom_UP2
let B1 be Element of rho R; :: according to UNIFORM3:def 1 :: thesis: ex B2 being Element of rho R st B2 c= B1 ~
B1 in rho R ;
then consider C1 being Subset of [:X,X:] such that
A1: B1 = C1 and
A2: R c= C1 ;
reconsider R1 = C1 as Relation of X ;
A3: R ~ c= R1 ~ by A2, SYSREL:11;
R in rho R ;
then reconsider B2 = R as Element of rho R ;
B2 c= B1 ~ by A3, A1, RELAT_2:13;
hence ex B2 being Element of rho R st B2 c= B1 ~ ; :: thesis: verum