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:
let x be object ; :: 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 ; :: thesis: verum
end;
suppose not R is empty ; :: thesis:
then consider z being object such that
A3: R = {[z,z]} by Th4;
let x be object ; :: 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 A4: x in (dom R) \/ (rng R) by RELAT_1:def 6;
( dom R = {z} & rng R = {z} ) by ;
then x = z by ;
hence [x,x] in R by ; :: thesis: verum
end;
end;
end;
A5: R is_transitive_in field R
proof
per cases ( R is empty or not R is empty ) ;
suppose A6: R is empty ; :: thesis:
let x, y, z be object ; :: 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 that
x in field R and
y in field R and
z in field R and
A7: [x,y] in R and
[y,z] in R ; :: thesis: [x,z] in R
thus [x,z] in R by A6, A7; :: thesis: verum
end;
suppose A8: not R is empty ; :: thesis:
let x, y, z be object ; :: 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 that
x in field R and
y in field R and
z in field R and
A9: [x,y] in R and
A10: [y,z] in R ; :: thesis: [x,z] in R
consider a being object such that
A11: R = {[a,a]} by ;
[y,z] = [a,a] by ;
then A12: z = a by XTUPLE_0:1;
[x,y] = [a,a] by ;
then x = a by XTUPLE_0:1;
hence [x,z] in R by ; :: thesis: verum
end;
end;
end;
A13: R is_strongly_connected_in field R
proof
per cases ( R is empty or not R is empty ) ;
suppose A14: R is empty ; :: thesis:
let x, y be object ; :: 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 that
A15: x in field R and
y in field R ; :: thesis: ( [x,y] in R or [y,x] in R )
thus ( [x,y] in R or [y,x] in R ) by ; :: thesis: verum
end;
suppose A16: not R is empty ; :: thesis:
let x, y be object ; :: 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 that
A17: x in field R and
A18: y in field R ; :: thesis: ( [x,y] in R or [y,x] in R )
consider a being object such that
A19: R = {[a,a]} by ;
A20: ( dom R = {a} & rng R = {a} ) by ;
y in (dom R) \/ (rng R) by ;
then A21: y = a by ;
x in (dom R) \/ (rng R) by ;
then x = a by ;
hence ( [x,y] in R or [y,x] in R ) by ; :: thesis: verum
end;
end;
end;
R is_symmetric_in field R
proof
per cases ( R is empty or not R is empty ) ;
suppose A22: R is empty ; :: thesis:
let x, y be object ; :: 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 that
x in field R and
y in field R and
A23: [x,y] in R ; :: thesis: [y,x] in R
thus [y,x] in R by ; :: thesis: verum
end;
suppose A24: not R is empty ; :: thesis:
let x, y be object ; :: 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 that
x in field R and
y in field R and
A25: [x,y] in R ; :: thesis: [y,x] in R
consider a being object such that
A26: R = {[a,a]} by ;
[x,y] = [a,a] by ;
then ( x = a & y = a ) by XTUPLE_0:1;
hence [y,x] in R by ; :: 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, A13; :: thesis: verum