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 #);
field the InternalRel of OverloadedRSSign(# A,R,O,Ol,f,g #) = the carrier of OverloadedRSSign(# A,R,O,Ol,f,g #) by ORDERS_1:97;
then ( 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 #) & 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 9, RELAT_2:def 12, 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 ORDERS_2:def 4, ORDERS_2:def 5, ORDERS_2:def 6; :: thesis: verum