let A be partial non-empty UAStr ; :: thesis: for R being Equivalence_Relation of the carrier of A st R c= DomRel A holds
for i being Element of NAT holds
( R |^ (A,i) is total & R |^ (A,i) is symmetric & R |^ (A,i) is transitive )
let R be Equivalence_Relation of the carrier of A; :: thesis: ( R c= DomRel A implies for i being Element of NAT holds
( R |^ (A,i) is total & R |^ (A,i) is symmetric & R |^ (A,i) is transitive ) )
assume A1: R c= DomRel A ; :: thesis: for i being Element of NAT holds
( R |^ (A,i) is total & R |^ (A,i) is symmetric & R |^ (A,i) is transitive )
defpred S₁[ Nat] means ( R |^ (A,$1) c= DomRel A & R |^ (A,$1) is total & R |^ (A,$1) is symmetric & R |^ (A,$1) is transitive );
A2: S₁[ 0 ] by A1, Th15;

A3: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
A5: (R |^ (A,i)) |^ A c= R |^ (A,i) by Th19;
(R |^ (A,i)) |^ A = R |^ (A,(i + 1)) by Th16;
hence S₁[i + 1] by A4, A5, Th18, XBOOLE_1:1; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
hence for i being Element of NAT holds
( R |^ (A,i) is total & R |^ (A,i) is symmetric & R |^ (A,i) is transitive ) ; :: thesis: verum