now :: thesis: for x being object st x in the carrier of A holds
[x,x] in LimDomRel A
let x be object ; :: 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 :: thesis: for i being Element of NAT holds [a,a] in (DomRel A) |^ (A,i)
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 Th20;
hence [a,a] in (DomRel A) |^ (A,i) by EQREL_1:5; :: thesis: verum
end;
hence [x,x] in LimDomRel A by Def7; :: thesis: verum
end;
then A1: LimDomRel A is_reflexive_in the carrier of A ;
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 :: thesis: for x, y being object st x in the carrier of A & y in the carrier of A & [x,y] in LimDomRel A holds
[y,x] in LimDomRel A
let x, y be object ; :: 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 :: thesis: for i being Element of NAT holds [b,a] in (DomRel A) |^ (A,i)
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 Th20;
[a,b] in (DomRel A) |^ (A,i) by A6, Def7;
hence [b,a] in (DomRel A) |^ (A,i) by A7, EQREL_1:6; :: thesis: verum
end;
hence [y,x] in LimDomRel A by Def7; :: thesis: verum
end;
then LimDomRel A is_symmetric_in the carrier of A ;
hence LimDomRel A is symmetric by A3; :: thesis: LimDomRel A is transitive
now :: thesis: for x, y, z being object st 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 holds
[x,z] in LimDomRel A
let x, y, z be object ; :: 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 :: thesis: for i being Element of NAT holds [a,c] in (DomRel A) |^ (A,i)
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 Th20;
A14: [a,b] in (DomRel A) |^ (A,i) by A11, Def7;
[b,c] in (DomRel A) |^ (A,i) by A12, Def7;
hence [a,c] in (DomRel A) |^ (A,i) by A13, A14, EQREL_1:7; :: thesis: verum
end;
hence [x,z] in LimDomRel A by Def7; :: thesis: verum
end;
then LimDomRel A is_transitive_in the carrier of A ;
hence LimDomRel A is transitive by A3; :: thesis: verum