per cases ( A is empty or B is empty or ( not A is empty & not B is empty ) ) ;
suppose ( A is empty or B is empty ) ; :: thesis: [:A,B:] is trivial
hence [:A,B:] is trivial ; :: thesis: verum
end;
suppose that A1: not A is empty and
A2: not B is empty ; :: thesis: [:A,B:] is trivial
consider a being object such that
A3: A = {a} by A1, Th130;
consider b being object such that
A4: B = {b} by A2, Th130;
[:A,B:] = {[a,b]} by A3, A4, Th28;
hence [:A,B:] is trivial ; :: thesis: verum
end;
end;