let A be non empty reflexive RelStr ; :: thesis: for a being Element of A holds {a} is Chain of A
let a be Element of A; :: thesis: {a} is Chain of A
A1: the InternalRel of A is_reflexive_in the carrier of A by Def2;
{a} is strongly_connected
proof
let x1, x2 be object ; :: according to RELAT_2:def 7,ORDERS_2:def 7 :: thesis: ( not x1 in {a} or not x2 in {a} or [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A )
assume ( x1 in {a} & x2 in {a} ) ; :: thesis: ( [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A )
then ( x1 = a & x2 = a ) by TARSKI:def 1;
hence ( [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A ) by A1; :: thesis: verum
end;
hence {a} is Chain of A ; :: thesis: verum