let p, q be finite set ; :: thesis: ( p c< q implies card p < card q )
assume A1: ( p c= q & p <> q ) ; :: according to XBOOLE_0:def 8 :: thesis: card p < card q
then X: card p <= card q by NAT_1:44;

now

assume A2: card p = card q ; :: thesis: contradiction
p,q are_c=-comparable by A1, XBOOLE_0:def 9;
hence contradiction by A1, A2, Th19; :: thesis: verum

end;

hence card p < card q by X, XXREAL_0:1; :: thesis: verum