let A be complex-membered set ; :: thesis: for a, b being Complex st b in A holds
b / a in A /// a
let a, b be Complex; :: thesis: ( b in A implies b / a in A /// a )
a in {a} by TARSKI:def 1;
hence ( b in A implies b / a in A /// a ) by Th116; :: thesis: verum