:: RELAT_2 semantic presentation

definition
let c1 be Relation;
let c2 be set ;
pred c1 is_reflexive_in c2 means :Def1: :: RELAT_2:def 1
for b1 being set st b1 in a2 holds
[b1,b1] in a1;
pred c1 is_irreflexive_in c2 means :Def2: :: RELAT_2:def 2
for b1 being set st b1 in a2 holds
not [b1,b1] in a1;
pred c1 is_symmetric_in c2 means :Def3: :: RELAT_2:def 3
for b1, b2 being set st b1 in a2 & b2 in a2 & [b1,b2] in a1 holds
[b2,b1] in a1;
pred c1 is_antisymmetric_in c2 means :Def4: :: RELAT_2:def 4
for b1, b2 being set st b1 in a2 & b2 in a2 & [b1,b2] in a1 & [b2,b1] in a1 holds
b1 = b2;
pred c1 is_asymmetric_in c2 means :Def5: :: RELAT_2:def 5
for b1, b2 being set st b1 in a2 & b2 in a2 & [b1,b2] in a1 holds
not [b2,b1] in a1;
pred c1 is_connected_in c2 means :Def6: :: RELAT_2:def 6
for b1, b2 being set st b1 in a2 & b2 in a2 & b1 <> b2 & not [b1,b2] in a1 holds
[b2,b1] in a1;
pred c1 is_strongly_connected_in c2 means :Def7: :: RELAT_2:def 7
for b1, b2 being set st b1 in a2 & b2 in a2 & not [b1,b2] in a1 holds
[b2,b1] in a1;
pred c1 is_transitive_in c2 means :Def8: :: RELAT_2:def 8
for b1, b2, b3 being set st b1 in a2 & b2 in a2 & b3 in a2 & [b1,b2] in a1 & [b2,b3] in a1 holds
[b1,b3] in a1;
end;

:: deftheorem Def1 defines is_reflexive_in RELAT_2:def 1 :
for b1 being Relation
for b2 being set holds
( b1 is_reflexive_in b2 iff for b3 being set st b3 in b2 holds
[b3,b3] in b1 );

:: deftheorem Def2 defines is_irreflexive_in RELAT_2:def 2 :
for b1 being Relation
for b2 being set holds
( b1 is_irreflexive_in b2 iff for b3 being set st b3 in b2 holds
not [b3,b3] in b1 );

:: deftheorem Def3 defines is_symmetric_in RELAT_2:def 3 :
for b1 being Relation
for b2 being set holds
( b1 is_symmetric_in b2 iff for b3, b4 being set st b3 in b2 & b4 in b2 & [b3,b4] in b1 holds
[b4,b3] in b1 );

:: deftheorem Def4 defines is_antisymmetric_in RELAT_2:def 4 :
for b1 being Relation
for b2 being set holds
( b1 is_antisymmetric_in b2 iff for b3, b4 being set st b3 in b2 & b4 in b2 & [b3,b4] in b1 & [b4,b3] in b1 holds
b3 = b4 );

:: deftheorem Def5 defines is_asymmetric_in RELAT_2:def 5 :
for b1 being Relation
for b2 being set holds
( b1 is_asymmetric_in b2 iff for b3, b4 being set st b3 in b2 & b4 in b2 & [b3,b4] in b1 holds
not [b4,b3] in b1 );

:: deftheorem Def6 defines is_connected_in RELAT_2:def 6 :
for b1 being Relation
for b2 being set holds
( b1 is_connected_in b2 iff for b3, b4 being set st b3 in b2 & b4 in b2 & b3 <> b4 & not [b3,b4] in b1 holds
[b4,b3] in b1 );

:: deftheorem Def7 defines is_strongly_connected_in RELAT_2:def 7 :
for b1 being Relation
for b2 being set holds
( b1 is_strongly_connected_in b2 iff for b3, b4 being set st b3 in b2 & b4 in b2 & not [b3,b4] in b1 holds
[b4,b3] in b1 );

:: deftheorem Def8 defines is_transitive_in RELAT_2:def 8 :
for b1 being Relation
for b2 being set holds
( b1 is_transitive_in b2 iff for b3, b4, b5 being set st b3 in b2 & b4 in b2 & b5 in b2 & [b3,b4] in b1 & [b4,b5] in b1 holds
[b3,b5] in b1 );

definition
let c1 be Relation;
attr a1 is reflexive means :Def9: :: RELAT_2:def 9
a1 is_reflexive_in field a1;
attr a1 is irreflexive means :Def10: :: RELAT_2:def 10
a1 is_irreflexive_in field a1;
attr a1 is symmetric means :Def11: :: RELAT_2:def 11
a1 is_symmetric_in field a1;
attr a1 is antisymmetric means :Def12: :: RELAT_2:def 12
a1 is_antisymmetric_in field a1;
attr a1 is asymmetric means :Def13: :: RELAT_2:def 13
a1 is_asymmetric_in field a1;
attr a1 is connected means :Def14: :: RELAT_2:def 14
a1 is_connected_in field a1;
attr a1 is strongly_connected means :Def15: :: RELAT_2:def 15
a1 is_strongly_connected_in field a1;
attr a1 is transitive means :Def16: :: RELAT_2:def 16
a1 is_transitive_in field a1;
end;

:: deftheorem Def9 defines reflexive RELAT_2:def 9 :
for b1 being Relation holds
( b1 is reflexive iff b1 is_reflexive_in field b1 );

:: deftheorem Def10 defines irreflexive RELAT_2:def 10 :
for b1 being Relation holds
( b1 is irreflexive iff b1 is_irreflexive_in field b1 );

:: deftheorem Def11 defines symmetric RELAT_2:def 11 :
for b1 being Relation holds
( b1 is symmetric iff b1 is_symmetric_in field b1 );

:: deftheorem Def12 defines antisymmetric RELAT_2:def 12 :
for b1 being Relation holds
( b1 is antisymmetric iff b1 is_antisymmetric_in field b1 );

:: deftheorem Def13 defines asymmetric RELAT_2:def 13 :
for b1 being Relation holds
( b1 is asymmetric iff b1 is_asymmetric_in field b1 );

:: deftheorem Def14 defines connected RELAT_2:def 14 :
for b1 being Relation holds
( b1 is connected iff b1 is_connected_in field b1 );

:: deftheorem Def15 defines strongly_connected RELAT_2:def 15 :
for b1 being Relation holds
( b1 is strongly_connected iff b1 is_strongly_connected_in field b1 );

:: deftheorem Def16 defines transitive RELAT_2:def 16 :
for b1 being Relation holds
( b1 is transitive iff b1 is_transitive_in field b1 );

theorem Th1: :: RELAT_2:1
canceled;

theorem Th2: :: RELAT_2:2
canceled;

theorem Th3: :: RELAT_2:3
canceled;

theorem Th4: :: RELAT_2:4
canceled;

theorem Th5: :: RELAT_2:5
canceled;

theorem Th6: :: RELAT_2:6
canceled;

theorem Th7: :: RELAT_2:7
canceled;

theorem Th8: :: RELAT_2:8
canceled;

theorem Th9: :: RELAT_2:9
canceled;

theorem Th10: :: RELAT_2:10
canceled;

theorem Th11: :: RELAT_2:11
canceled;

theorem Th12: :: RELAT_2:12
canceled;

theorem Th13: :: RELAT_2:13
canceled;

theorem Th14: :: RELAT_2:14
canceled;

theorem Th15: :: RELAT_2:15
canceled;

theorem Th16: :: RELAT_2:16
canceled;

theorem Th17: :: RELAT_2:17
for b1 being Relation holds
( b1 is reflexive iff id (field b1) c= b1 )
proof end;

theorem Th18: :: RELAT_2:18
for b1 being Relation holds
( b1 is irreflexive iff id (field b1) misses b1 )
proof end;

theorem Th19: :: RELAT_2:19
for b1 being set
for b2 being Relation holds
( b2 is_antisymmetric_in b1 iff b2 \ (id b1) is_asymmetric_in b1 )
proof end;

theorem Th20: :: RELAT_2:20
for b1 being set
for b2 being Relation st b2 is_asymmetric_in b1 holds
b2 \/ (id b1) is_antisymmetric_in b1
proof end;

theorem Th21: :: RELAT_2:21
canceled;

theorem Th22: :: RELAT_2:22
for b1 being Relation st b1 is symmetric & b1 is transitive holds
b1 is reflexive
proof end;

theorem Th23: :: RELAT_2:23
for b1 being set holds
( id b1 is symmetric & id b1 is transitive )
proof end;

theorem Th24: :: RELAT_2:24
for b1 being set holds
( id b1 is antisymmetric & id b1 is reflexive )
proof end;

theorem Th25: :: RELAT_2:25
for b1 being Relation st b1 is irreflexive & b1 is transitive holds
b1 is asymmetric
proof end;

theorem Th26: :: RELAT_2:26
for b1 being Relation st b1 is asymmetric holds
( b1 is irreflexive & b1 is antisymmetric )
proof end;

theorem Th27: :: RELAT_2:27
for b1 being Relation st b1 is reflexive holds
b1 ~ is reflexive
proof end;

theorem Th28: :: RELAT_2:28
for b1 being Relation st b1 is irreflexive holds
b1 ~ is irreflexive
proof end;

theorem Th29: :: RELAT_2:29
for b1 being Relation st b1 is reflexive holds
( dom b1 = dom (b1 ~ ) & rng b1 = rng (b1 ~ ) )
proof end;

theorem Th30: :: RELAT_2:30
for b1 being Relation holds
( b1 is symmetric iff b1 = b1 ~ )
proof end;

theorem Th31: :: RELAT_2:31
for b1, b2 being Relation st b1 is reflexive & b2 is reflexive holds
( b1 \/ b2 is reflexive & b1 /\ b2 is reflexive )
proof end;

theorem Th32: :: RELAT_2:32
for b1, b2 being Relation st b1 is irreflexive & b2 is irreflexive holds
( b1 \/ b2 is irreflexive & b1 /\ b2 is irreflexive )
proof end;

theorem Th33: :: RELAT_2:33
for b1, b2 being Relation st b1 is irreflexive holds
b1 \ b2 is irreflexive
proof end;

theorem Th34: :: RELAT_2:34
for b1 being Relation st b1 is symmetric holds
b1 ~ is symmetric by Th30;

theorem Th35: :: RELAT_2:35
for b1, b2 being Relation st b1 is symmetric & b2 is symmetric holds
( b1 \/ b2 is symmetric & b1 /\ b2 is symmetric & b1 \ b2 is symmetric )
proof end;

theorem Th36: :: RELAT_2:36
for b1 being Relation st b1 is asymmetric holds
b1 ~ is asymmetric
proof end;

theorem Th37: :: RELAT_2:37
for b1, b2 being Relation st b1 is asymmetric & b2 is asymmetric holds
b1 /\ b2 is asymmetric
proof end;

theorem Th38: :: RELAT_2:38
for b1, b2 being Relation st b1 is asymmetric holds
b1 \ b2 is asymmetric
proof end;

theorem Th39: :: RELAT_2:39
for b1 being Relation holds
( b1 is antisymmetric iff b1 /\ (b1 ~ ) c= id (dom b1) )
proof end;

theorem Th40: :: RELAT_2:40
for b1 being Relation st b1 is antisymmetric holds
b1 ~ is antisymmetric
proof end;

theorem Th41: :: RELAT_2:41
for b1, b2 being Relation st b1 is antisymmetric holds
( b1 /\ b2 is antisymmetric & b1 \ b2 is antisymmetric )
proof end;

theorem Th42: :: RELAT_2:42
for b1 being Relation st b1 is transitive holds
b1 ~ is transitive
proof end;

theorem Th43: :: RELAT_2:43
for b1, b2 being Relation st b1 is transitive & b2 is transitive holds
b1 /\ b2 is transitive
proof end;

theorem Th44: :: RELAT_2:44
for b1 being Relation holds
( b1 is transitive iff b1 * b1 c= b1 )
proof end;

theorem Th45: :: RELAT_2:45
for b1 being Relation holds
( b1 is connected iff [:(field b1),(field b1):] \ (id (field b1)) c= b1 \/ (b1 ~ ) )
proof end;

theorem Th46: :: RELAT_2:46
for b1 being Relation st b1 is strongly_connected holds
( b1 is connected & b1 is reflexive )
proof end;

theorem Th47: :: RELAT_2:47
for b1 being Relation holds
( b1 is strongly_connected iff [:(field b1),(field b1):] = b1 \/ (b1 ~ ) )
proof end;