per cases ( X = {} or X <> {} ) ;

suppose X = {} ; :: thesis: for b₁ being Relation of [:X,X:],X st b₁ is quasi_total holds
b₁ is total

hence for b₁ being Relation of [:X,X:],X st b₁ is quasi_total holds
b₁ is total ; :: thesis: verum

end;

suppose X <> {} ; :: thesis: for b₁ being Relation of [:X,X:],X st b₁ is quasi_total holds
b₁ is total

hence for b₁ being Relation of [:X,X:],X st b₁ is quasi_total holds
b₁ is total ; :: thesis: verum

end;

end;