now

let x be set ; :: thesis: ( x in the carrier of A implies [x,x] in LimDomRel A )
assume x in the carrier of A ; :: thesis: [x,x] in LimDomRel A
then reconsider a = x as Element of A ;

now

let i be Element of NAT ; :: thesis: [a,a] in (DomRel A) |^ (A,i)
( (DomRel A) |^ (A,i) is total & (DomRel A) |^ (A,i) is symmetric & (DomRel A) |^ (A,i) is transitive ) by Th22;
hence [a,a] in (DomRel A) |^ (A,i) by EQREL_1:5; :: thesis: verum

end;

hence [x,x] in LimDomRel A by Def8; :: thesis: verum

end;

then A1: LimDomRel A is_reflexive_in the carrier of A by RELAT_2:def 1;
then A2: dom (LimDomRel A) = the carrier of A by ORDERS_1:13;
A3: field (LimDomRel A) = the carrier of A by A1, ORDERS_1:13;
thus LimDomRel A is total by A2, PARTFUN1:def 2; :: thesis: ( LimDomRel A is symmetric & LimDomRel A is transitive )

now

let x, y be set ; :: thesis: ( x in the carrier of A & y in the carrier of A & [x,y] in LimDomRel A implies [y,x] in LimDomRel A )
assume that
A4: x in the carrier of A and
A5: y in the carrier of A ; :: thesis: ( [x,y] in LimDomRel A implies [y,x] in LimDomRel A )
reconsider a = x, b = y as Element of A by A4, A5;
assume A6: [x,y] in LimDomRel A ; :: thesis: [y,x] in LimDomRel A

now

let i be Element of NAT ; :: thesis: [b,a] in (DomRel A) |^ (A,i)
A7: ( (DomRel A) |^ (A,i) is total & (DomRel A) |^ (A,i) is symmetric & (DomRel A) |^ (A,i) is transitive ) by Th22;
[a,b] in (DomRel A) |^ (A,i) by A6, Def8;
hence [b,a] in (DomRel A) |^ (A,i) by A7, EQREL_1:6; :: thesis: verum

end;

hence [y,x] in LimDomRel A by Def8; :: thesis: verum

end;

then LimDomRel A is_symmetric_in the carrier of A by RELAT_2:def 3;
hence LimDomRel A is symmetric by A3, RELAT_2:def 11; :: thesis: LimDomRel A is transitive

now

let x, y, z be set ; :: thesis: ( x in the carrier of A & y in the carrier of A & z in the carrier of A & [x,y] in LimDomRel A & [y,z] in LimDomRel A implies [x,z] in LimDomRel A )
assume that
A8: x in the carrier of A and
A9: y in the carrier of A and
A10: z in the carrier of A ; :: thesis: ( [x,y] in LimDomRel A & [y,z] in LimDomRel A implies [x,z] in LimDomRel A )
reconsider a = x, b = y, c = z as Element of A by A8, A9, A10;
assume that
A11: [x,y] in LimDomRel A and
A12: [y,z] in LimDomRel A ; :: thesis: [x,z] in LimDomRel A

now

let i be Element of NAT ; :: thesis: [a,c] in (DomRel A) |^ (A,i)
A13: ( (DomRel A) |^ (A,i) is total & (DomRel A) |^ (A,i) is symmetric & (DomRel A) |^ (A,i) is transitive ) by Th22;
A14: [a,b] in (DomRel A) |^ (A,i) by A11, Def8;
[b,c] in (DomRel A) |^ (A,i) by A12, Def8;
hence [a,c] in (DomRel A) |^ (A,i) by A13, A14, EQREL_1:7; :: thesis: verum

end;

hence [x,z] in LimDomRel A by Def8; :: thesis: verum

end;

then LimDomRel A is_transitive_in the carrier of A by RELAT_2:def 8;
hence LimDomRel A is transitive by A3, RELAT_2:def 16; :: thesis: verum