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 S1[ Nat] means ( R |^ (A,$1) c= DomRel A & R |^ (A,$1) is total & R |^ (A,$1) is symmetric & R |^ (A,$1) is transitive );
A2: S1[ 0 ] by A1, Th15;
A3: now :: thesis: for i being Nat st S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A4: S1[i] ; :: thesis: S1[i + 1]
A5: (R |^ (A,i)) |^ A c= R |^ (A,i) by Th19;
(R |^ (A,i)) |^ A = R |^ (A,(i + 1)) by Th16;
hence S1[i + 1] by A4, A5, Th18, XBOOLE_1:1; :: thesis: verum
end;
for i being Nat holds S1[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