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 b1 being set st b1 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 b1 being set st b1 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