let R be non empty discrete Poset; :: thesis: for C being Component of R ex x being Element of R st C = {x}
let C be Component of R; :: thesis: ex x being Element of R st C = {x}
consider x being object such that
A1: x in the carrier of R and
A2: C = Class ((Path_Rel R),x) by EQREL_1:def 3;
reconsider x1 = x as Element of R by A1;
take x1 ; :: thesis: C = {x1}
for y being object holds
( y in C iff y = x1 )
proof
let y be object ; :: thesis: ( y in C iff y = x1 )
hereby :: thesis: ( y = x1 implies y in C )
assume A3: y in C ; :: thesis: y = x1
then reconsider y1 = y as Element of R ;
[y,x] in Path_Rel R by A2, A3, EQREL_1:19;
then y1 = x1 by Th6;
hence y = x1 ; :: thesis: verum
end;
assume y = x1 ; :: thesis: y in C
hence y in C by A2, EQREL_1:20; :: thesis: verum
end;
hence C = {x1} by TARSKI:def 1; :: thesis: verum