let x, y be set ; :: thesis: ( <*x*>,<*y*> are_c=-comparable iff x = y )
thus ( <*x*>,<*y*> are_c=-comparable implies x = y ) :: thesis: ( x = y implies <*x*>,<*y*> are_c=-comparable )

proof

assume A1: <*x*>,<*y*> are_c=-comparable ; :: thesis: x = y
A2: ( len <*x*> = 1 & len <*y*> = 1 ) by FINSEQ_1:57;
A3: <*x*> = <*y*> by A1, A2, Th19;
A4: <*x*> . 1 = x by FINSEQ_1:57;
thus x = y by A3, A4, FINSEQ_1:57; :: thesis: verum

end;

thus ( x = y implies <*x*>,<*y*> are_c=-comparable ) ; :: thesis: verum