let A, O be non empty set ; :: thesis: for R being Order of A
for Ol being Equivalence_Relation of O
for f being Function of O,(A *)
for g being Function of O,A holds
( 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 reflexive & OverloadedRSSign(# A,R,O,Ol,f,g #) is transitive & OverloadedRSSign(# A,R,O,Ol,f,g #) is antisymmetric )
let R be Order of A; :: thesis: for Ol being Equivalence_Relation of O
for f being Function of O,(A *)
for g being Function of O,A holds
( 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 reflexive & OverloadedRSSign(# A,R,O,Ol,f,g #) is transitive & OverloadedRSSign(# A,R,O,Ol,f,g #) is antisymmetric )
let Ol be Equivalence_Relation of O; :: thesis: for f being Function of O,(A *)
for g being Function of O,A holds
( 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 reflexive & OverloadedRSSign(# A,R,O,Ol,f,g #) is transitive & OverloadedRSSign(# A,R,O,Ol,f,g #) is antisymmetric )
let f be Function of O,(A *); :: thesis: for g being Function of O,A holds
( 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 reflexive & OverloadedRSSign(# A,R,O,Ol,f,g #) is transitive & OverloadedRSSign(# A,R,O,Ol,f,g #) is antisymmetric )
let g be Function of O,A; :: thesis: ( 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 reflexive & OverloadedRSSign(# A,R,O,Ol,f,g #) is transitive & OverloadedRSSign(# A,R,O,Ol,f,g #) is antisymmetric )
set RS0 = OverloadedRSSign(# A,R,O,Ol,f,g #);
A1: field the InternalRel of OverloadedRSSign(# A,R,O,Ol,f,g #) = the carrier of OverloadedRSSign(# A,R,O,Ol,f,g #) by ORDERS_1:12;
then A2: the InternalRel of OverloadedRSSign(# A,R,O,Ol,f,g #) is_antisymmetric_in the carrier of OverloadedRSSign(# A,R,O,Ol,f,g #) by RELAT_2:def 12;
( the InternalRel of OverloadedRSSign(# A,R,O,Ol,f,g #) is_reflexive_in the carrier of OverloadedRSSign(# A,R,O,Ol,f,g #) & the InternalRel of OverloadedRSSign(# A,R,O,Ol,f,g #) is_transitive_in the carrier of OverloadedRSSign(# A,R,O,Ol,f,g #) ) by A1, RELAT_2:def 9, RELAT_2:def 16;
hence ( 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 reflexive & OverloadedRSSign(# A,R,O,Ol,f,g #) is transitive & OverloadedRSSign(# A,R,O,Ol,f,g #) is antisymmetric ) by A2, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4; :: thesis: verum