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₁[ Element of 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, Th17;

A3: now

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
( (R |^ A,i) |^ A c= R |^ A,i & (R |^ A,i) |^ A = R |^ A,(i + 1) ) by Th18, Th21;
hence S₁[i + 1] by A4, Th20, XBOOLE_1:1; :: thesis: verum

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(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