per cases ( cB is empty or not cB is empty ) ;

suppose cB is empty ; :: thesis: not <.cB.] is empty

hence not <.cB.] is empty by CARDFIL2:15; :: thesis: verum

end;

suppose A1: not cB is empty ; :: thesis: not <.cB.] is empty

cB c= <.cB.] by CARDFIL2:18;
hence not <.cB.] is empty by A1; :: thesis: verum

end;

end;