let X, Y be set ; :: thesis: for F being a_partition of Y st Y c< X holds
F \/ {(X \ Y)} is a_partition of X
let F be a_partition of Y; :: thesis: ( Y c< X implies F \/ {(X \ Y)} is a_partition of X )
assume A: Y c< X ; :: thesis: F \/ {(X \ Y)} is a_partition of X
then Ba: X \ Y <> {} by XBOOLE_1:105;
Y c= X by A, XBOOLE_0:def 8;
then C: Y \/ (X \ Y) = X by XBOOLE_1:45;
{(X \ Y)} is a_partition of X \ Y by Ba, EQREL_1:48;
hence F \/ {(X \ Y)} is a_partition of X by XBOOLE_1:79, C, SPpart0; :: thesis: verum