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;