let p, q be finite set ; :: thesis: ( p c< q implies card p < card q )
assume that
A1: p c= q and
A2: p <> q ; :: according to XBOOLE_0:def 8 :: thesis: card p < card q
A3: card p <= card q by A1, NAT_1:43;
p,q are_c=-comparable by A1;
hence card p < card q by A3, A2, Th3, XXREAL_0:1; :: thesis: verum