set A = the non empty set ;
set R = the Order of the non empty set ;
set O = the non empty set ;
set Ol = the Equivalence_Relation of the non empty set ;
set f = the Function of the non empty set ,( the non empty set *);
set g = the Function of the non empty set , the non empty set ;
take OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) ; :: thesis: ( OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is strict & not OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is empty & not OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is void & OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is order-sorted )
thus ( OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is strict & not OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is empty & not OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is void & OverloadedRSSign(# the non empty set , the Order of the non empty set , the non empty set , the Equivalence_Relation of the non empty set , the Function of the non empty set ,( the non empty set *), the Function of the non empty set , the non empty set #) is order-sorted ) ; :: thesis: verum