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 Z: 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 )
thus R is reflexive :: thesis: ( R is irreflexive & R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )

proof

for x being set st x in {} holds
[x,x] in {} ;
then {} is_reflexive_in field {} by RELAT_2:def 1;
hence R is reflexive by Z, RELAT_2:def 9; :: thesis: verum

end;

thus R is irreflexive :: thesis: ( R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )

proof

{} is_irreflexive_in field {}

proof

let x be set ; :: according to RELAT_2:def 2 :: thesis: ( not x in field {} or not [x,x] in {} )
assume x in field {} ; :: thesis: not [x,x] in {}
thus not [x,x] in {} ; :: thesis: verum

end;

hence R is irreflexive by Z, RELAT_2:def 10; :: thesis: verum

end;

thus R is symmetric :: thesis: ( R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )

proof

let x be set ; :: according to RELAT_2:def 3,RELAT_2:def 11 :: thesis: for b₁ being set holds
( not x in field R or not b₁ in field R or not [x,b₁] in R or [b₁,x] in R )
let y be set ; :: thesis: ( not x in field R or not y in field R or not [x,y] in R or [y,x] in R )
assume ( x in field R & y in field R & [x,y] in R ) ; :: thesis: [y,x] in R
hence [y,x] in R by Z; :: thesis: verum

end;

thus R is antisymmetric :: thesis: ( R is asymmetric & R is connected & R is strongly_connected & R is transitive )

proof

{} is_antisymmetric_in field {}

proof

let x be set ; :: according to RELAT_2:def 4 :: thesis: for b₁ being set holds
( not x in field {} or not b₁ in field {} or not [x,b₁] in {} or not [b₁,x] in {} or x = b₁ )
let y be set ; :: thesis: ( not x in field {} or not y in field {} or not [x,y] in {} or not [y,x] in {} or x = y )
assume ( x in field {} & y in field {} & [x,y] in {} & [y,x] in {} ) ; :: thesis: x = y
hence x = y ; :: thesis: verum

end;

hence R is antisymmetric by Z, RELAT_2:def 12; :: thesis: verum

end;

thus R is asymmetric :: thesis: ( R is connected & R is strongly_connected & R is transitive )

proof

{} is_asymmetric_in field {}

proof

let x be set ; :: according to RELAT_2:def 5 :: thesis: for b₁ being set holds
( not x in field {} or not b₁ in field {} or not [x,b₁] in {} or not [b₁,x] in {} )
let y be set ; :: thesis: ( not x in field {} or not y in field {} or not [x,y] in {} or not [y,x] in {} )
assume ( x in field {} & y in field {} & [x,y] in {} ) ; :: thesis: not [y,x] in {}
thus not [y,x] in {} ; :: thesis: verum

end;

hence R is asymmetric by Z, RELAT_2:def 13; :: thesis: verum

end;

thus R is connected :: thesis: ( R is strongly_connected & R is transitive )

proof

{} is_connected_in field {}

proof

let x be set ; :: according to RELAT_2:def 6 :: thesis: for b₁ being set holds
( not x in field {} or not b₁ in field {} or x = b₁ or [x,b₁] in {} or [b₁,x] in {} )
let y be set ; :: thesis: ( not x in field {} or not y in field {} or x = y or [x,y] in {} or [y,x] in {} )
assume ( x in field {} & y in field {} & x <> y ) ; :: thesis: ( [x,y] in {} or [y,x] in {} )
hence ( [x,y] in {} or [y,x] in {} ) ; :: thesis: verum

end;

hence R is connected by Z, RELAT_2:def 14; :: thesis: verum

end;

thus R is strongly_connected :: thesis: R is transitive

proof

{} is_strongly_connected_in field {}

proof

let x be set ; :: according to RELAT_2:def 7 :: thesis: for b₁ being set holds
( not x in field {} or not b₁ in field {} or [x,b₁] in {} or [b₁,x] in {} )
let y be set ; :: thesis: ( not x in field {} or not y in field {} or [x,y] in {} or [y,x] in {} )
assume ( x in field {} & y in field {} ) ; :: thesis: ( [x,y] in {} or [y,x] in {} )
hence ( [x,y] in {} or [y,x] in {} ) ; :: thesis: verum

end;

hence R is strongly_connected by Z, RELAT_2:def 15; :: thesis: verum

end;

thus R is transitive :: thesis: verum

proof

{} is_transitive_in field {}

proof

let x be set ; :: according to RELAT_2:def 8 :: thesis: for b₁, b₂ being set holds
( not x in field {} or not b₁ in field {} or not b₂ in field {} or not [x,b₁] in {} or not [b₁,b₂] in {} or [x,b₂] in {} )
let y, z be set ; :: thesis: ( not x in field {} or not y in field {} or not z in field {} or not [x,y] in {} or not [y,z] in {} or [x,z] in {} )
assume ( x in field {} & y in field {} & z in field {} & [x,y] in {} & [y,z] in {} ) ; :: thesis: [x,z] in {}
hence [x,z] in {} ; :: thesis: verum

end;

hence R is transitive by Z, RELAT_2:def 16; :: thesis: verum

end;