thus ( s is relational implies ex IT being set st IT is Function of ((abs (ar s)) -tuples_on U),BOOLEAN ) :: thesis: ( not s is relational implies ex b₁ being set st b₁ is Function of ((abs (ar s)) -tuples_on U),U )

proof

assume s is relational ; :: thesis: ex IT being set st IT is Function of ((abs (ar s)) -tuples_on U),BOOLEAN
take the Function of ((abs (ar s)) -tuples_on U),BOOLEAN ; :: thesis: the Function of ((abs (ar s)) -tuples_on U),BOOLEAN is Function of ((abs (ar s)) -tuples_on U),BOOLEAN
thus the Function of ((abs (ar s)) -tuples_on U),BOOLEAN is Function of ((abs (ar s)) -tuples_on U),BOOLEAN ; :: thesis: verum

end;

assume not s is relational ; :: thesis: ex b₁ being set st b₁ is Function of ((abs (ar s)) -tuples_on U),U
take the Function of ((abs (ar s)) -tuples_on U),U ; :: thesis: the Function of ((abs (ar s)) -tuples_on U),U is Function of ((abs (ar s)) -tuples_on U),U
thus the Function of ((abs (ar s)) -tuples_on U),U is Function of ((abs (ar s)) -tuples_on U),U ; :: thesis: verum