let R be Relation; :: thesis: ( R is empty implies ( R is reflexive & R is irreflexive & R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive ) )
assume A1: R is empty ; :: thesis: ( R is reflexive & R is irreflexive & R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
{} is_reflexive_in field {} ;
hence R is reflexive by A1; :: thesis: ( R is irreflexive & R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
{} is_irreflexive_in field {} ;
hence R is irreflexive by A1; :: thesis: ( R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
thus R is symmetric :: thesis: ( R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
proof
let x, y be object ; :: according to RELAT_2:def 3,RELAT_2:def 11 :: thesis: ( not x in field R or not y in field R or not [x,y] in R or [y,x] in R )
assume that
x in field R and
y in field R and
A2: [x,y] in R ; :: thesis: [y,x] in R
thus [y,x] in R by A1, A2; :: thesis: verum
end;
{} is_antisymmetric_in field {} ;
hence R is antisymmetric by A1; :: thesis: ( R is asymmetric & R is connected & R is strongly_connected & R is transitive )
{} is_asymmetric_in field {} ;
hence R is asymmetric by A1; :: thesis: ( R is connected & R is strongly_connected & R is transitive )
{} is_connected_in field {} ;
hence R is connected by A1; :: thesis: ( R is strongly_connected & R is transitive )
{} is_strongly_connected_in field {} ;
hence R is strongly_connected by A1; :: thesis: R is transitive
{} is_transitive_in field {} ;
hence R is transitive by A1; :: thesis: verum