let R be Relation of X,X; :: thesis: ( R is trivial & R is reflexive & R is symmetric & R is transitive & R is strongly_connected )
A1: R is_reflexive_in field R

proof

per cases ( R is empty or not R is empty ) ;

suppose A2: R is empty ; :: thesis: R is_reflexive_in field R

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in field R or [x,x] in R )
assume x in field R ; :: thesis: [x,x] in R
hence [x,x] in R by A2, RELAT_1:63; :: thesis: verum

end;

suppose not R is empty ; :: thesis: R is_reflexive_in field R

then consider z being set such that
A3: R = {[z,z]} by Th4;
A4: ( dom R = {z} & rng R = {z} ) by A3, RELAT_1:23;
let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in field R or [x,x] in R )
assume x in field R ; :: thesis: [x,x] in R
then x in (dom R) \/ (rng R) by RELAT_1:def 6;
then x = z by A4, TARSKI:def 1;
hence [x,x] in R by A3, TARSKI:def 1; :: thesis: verum

end;

end;

end;

A5: R is_symmetric_in field R

proof

per cases ( R is empty or not R is empty ) ;

suppose A6: R is empty ; :: thesis: R is_symmetric_in field R

let x, y be set ; :: according to RELAT_2:def 3 :: 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 A6; :: thesis: verum

end;

suppose not R is empty ; :: thesis: R is_symmetric_in field R

then consider a being set such that
A7: R = {[a,a]} by Th4;
let x, y be set ; :: according to RELAT_2:def 3 :: 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
then [x,y] = [a,a] by A7, TARSKI:def 1;
then ( x = a & y = a ) by ZFMISC_1:33;
hence [y,x] in R by A7, TARSKI:def 1; :: thesis: verum

end;

end;

end;

A8: R is_transitive_in field R

proof

per cases ( R is empty or not R is empty ) ;

suppose A9: R is empty ; :: thesis: R is_transitive_in field R

let x, y, z be set ; :: according to RELAT_2:def 8 :: thesis: ( not x in field R or not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume ( x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
hence [x,z] in R by A9; :: thesis: verum

end;

suppose not R is empty ; :: thesis: R is_transitive_in field R

then consider a being set such that
A10: R = {[a,a]} by Th4;
let x, y, z be set ; :: according to RELAT_2:def 8 :: thesis: ( not x in field R or not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume ( x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
then ( [x,y] = [a,a] & [y,z] = [a,a] ) by A10, TARSKI:def 1;
then ( x = a & y = a & z = a ) by ZFMISC_1:33;
hence [x,z] in R by A10, TARSKI:def 1; :: thesis: verum

end;

end;

end;

R is_strongly_connected_in field R

proof

per cases ( R is empty or not R is empty ) ;

suppose A11: R is empty ; :: thesis: R is_strongly_connected_in field R

let x, y be set ; :: according to RELAT_2:def 7 :: thesis: ( not x in field R or not y in field R or [x,y] in R or [y,x] in R )
assume ( x in field R & y in field R ) ; :: thesis: ( [x,y] in R or [y,x] in R )
hence ( [x,y] in R or [y,x] in R ) by A11, RELAT_1:63; :: thesis: verum

end;

suppose not R is empty ; :: thesis: R is_strongly_connected_in field R

then consider a being set such that
A12: R = {[a,a]} by Th4;
A13: ( dom R = {a} & rng R = {a} ) by A12, RELAT_1:23;
let x, y be set ; :: according to RELAT_2:def 7 :: thesis: ( not x in field R or not y in field R or [x,y] in R or [y,x] in R )
assume ( x in field R & y in field R ) ; :: thesis: ( [x,y] in R or [y,x] in R )
then ( x in (dom R) \/ (rng R) & y in (dom R) \/ (rng R) ) by RELAT_1:def 6;
then ( x = a & y = a ) by A13, TARSKI:def 1;
hence ( [x,y] in R or [y,x] in R ) by A12, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence ( R is trivial & R is reflexive & R is symmetric & R is transitive & R is strongly_connected ) by A1, A5, A8, RELAT_2:def 9, RELAT_2:def 11, RELAT_2:def 15, RELAT_2:def 16; :: thesis: verum