let x be set ; :: thesis: {x} is c=-linear
let y, z be set ; :: according to ORDINAL1:def 8 :: thesis: ( not y in {x} or not z in {x} or y,z are_c=-comparable )
assume that
A1: y in {x} and
A2: z in {x} ; :: thesis: y,z are_c=-comparable
y = x by A1, TARSKI:def 1;
hence y,z are_c=-comparable by A2, TARSKI:def 1; :: thesis: verum