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 A1: Y c< X ; :: thesis: F \/ {(X \ Y)} is a_partition of X
then A2: X \ Y <> {} by XBOOLE_1:105;
Y c= X by A1;
then A3: Y \/ (X \ Y) = X by XBOOLE_1:45;
{(X \ Y)} is a_partition of X \ Y by A2, EQREL_1:39;
hence F \/ {(X \ Y)} is a_partition of X by A3, Th3, XBOOLE_1:79; :: thesis: verum