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