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

proof

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

end;

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