let p, q be finite set ; :: thesis: ( p,q are_c=-comparable & card p = card q implies p = q )
assume that
A1: ( p c= q or q c= p ) and
A2: card p = card q ; :: according to XBOOLE_0:def 9 :: thesis: p = q

per cases ( p c= q or q c= p ) by A1;

suppose p c= q ; :: thesis: p = q

hence p = q by A2, Lm1; :: thesis: verum

end;

suppose q c= p ; :: thesis: p = q

hence p = q by A2, Lm1; :: thesis: verum

end;

end;