per cases ( X = {} or X <> {} ) ;
suppose X = {} ; :: thesis: for b1 being Relation of X,X st b1 is quasi_total holds
b1 is total
hence for b1 being Relation of X,X st b1 is quasi_total holds
b1 is total ; :: thesis: verum
end;
suppose X <> {} ; :: thesis: for b1 being Relation of X,X st b1 is quasi_total holds
b1 is total
hence for b1 being Relation of X,X st b1 is quasi_total holds
b1 is total ; :: thesis: verum
end;
end;