let X be set ; :: thesis: for R being total reflexive Relation of X holds rho R is axiom_UP1
let R be total reflexive Relation of X; :: thesis: rho R is axiom_UP1
now :: thesis: for B being Element of rho R holds id X c= B
let B be Element of rho R; :: thesis: id X c= B
B in rho R ;
then consider C being Subset of [:X,X:] such that
A1: B = C and
A2: R c= C ;
A3: field R = X by ORDERS_1:12;
id X c= R
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in id X or t in R )
assume A4: t in id X ; :: thesis: t in R
then consider a, b being object such that
a in X and
A5: b in X and
A6: t = [a,b] by ZFMISC_1:def 2;
a = b by A4, A6, RELAT_1:def 10;
hence t in R by A5, A3, A6, RELAT_2:def 9, RELAT_2:def 1; :: thesis: verum
end;
hence id X c= B by A1, A2; :: thesis: verum
end;
hence rho R is axiom_UP1 ; :: thesis: verum