:: Basic Notions and Properties of Orthoposets
:: by Markus Moschner
::
:: Received February 11, 2003
:: Copyright (c) 2003-2011 Association of Mizar Users


begin

theorem :: OPOSET_1:1
canceled;

theorem :: OPOSET_1:2
canceled;

theorem :: OPOSET_1:3
canceled;

theorem :: OPOSET_1:4
for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st x <= y holds
( sup {x,y} = y & inf {x,y} = x )
proof end;

theorem :: OPOSET_1:5
canceled;

theorem :: OPOSET_1:6
canceled;

theorem :: OPOSET_1:7
canceled;

theorem :: OPOSET_1:8
canceled;

theorem :: OPOSET_1:9
canceled;

theorem :: OPOSET_1:10
canceled;

theorem :: OPOSET_1:11
canceled;

theorem :: OPOSET_1:12
canceled;

theorem :: OPOSET_1:13
canceled;

theorem :: OPOSET_1:14
canceled;

theorem :: OPOSET_1:15
canceled;

theorem :: OPOSET_1:16
canceled;

registration
let X be set ;
cluster Relation-like irreflexive asymmetric transitive Element of bool [:X,X:];
existence
ex b1 being Relation of X st
( b1 is irreflexive & b1 is asymmetric & b1 is transitive )
proof end;
end;

registration
let X be non empty set ;
let R be Relation of X;
let C be UnOp of X;
cluster OrthoRelStr(# X,R,C #) -> non empty ;
coherence
not OrthoRelStr(# X,R,C #) is empty ;
end;

registration
cluster non empty strict OrthoRelStr ;
existence
ex b1 being OrthoRelStr st
( not b1 is empty & b1 is strict )
proof end;
end;

theorem :: OPOSET_1:17
canceled;

theorem :: OPOSET_1:18
canceled;

theorem :: OPOSET_1:19
canceled;

registration
let O be non empty OrthoRelStr ;
cluster Relation-like Function-like non empty V14( the carrier of O) V15( the carrier of O, the carrier of O) V243() Element of bool [: the carrier of O, the carrier of O:];
existence
ex b1 being Function of O,O st b1 is involutive
proof end;
end;

definition
canceled;
canceled;
canceled;
func TrivOrthoRelStr -> strict OrthoRelStr equals :Def4: :: OPOSET_1:def 4
 OrthoRelStr(# 1,(id 1),op1 #);
coherence
OrthoRelStr(# 1,(id 1),op1 #) is strict OrthoRelStr ;
end;

:: deftheorem OPOSET_1:def 1 :
canceled;

:: deftheorem OPOSET_1:def 2 :
canceled;

:: deftheorem OPOSET_1:def 3 :
canceled;

:: deftheorem Def4 defines TrivOrthoRelStr OPOSET_1:def 4 :
TrivOrthoRelStr = OrthoRelStr(# 1,(id 1),op1 #);

notation
synonym TrivPoset for TrivOrthoRelStr ;
end;

registration
cluster TrivOrthoRelStr -> non empty trivial strict ;
coherence
( not TrivOrthoRelStr is empty & TrivOrthoRelStr is trivial ) by CARD_1:87, REALSET1:def 4;
end;

definition
func TrivAsymOrthoRelStr -> strict OrthoRelStr equals :: OPOSET_1:def 5
 OrthoRelStr(# 1,({} (1,1)),op1 #);
coherence
OrthoRelStr(# 1,({} (1,1)),op1 #) is strict OrthoRelStr ;
end;

:: deftheorem defines TrivAsymOrthoRelStr OPOSET_1:def 5 :
TrivAsymOrthoRelStr = OrthoRelStr(# 1,({} (1,1)),op1 #);

registration
cluster TrivAsymOrthoRelStr -> non empty strict ;
coherence
not TrivAsymOrthoRelStr is empty ;
end;

definition
let O be non empty OrthoRelStr ;
attr O is Dneg means :Def6: :: OPOSET_1:def 6
 ex f being Function of O,O st
( f = the Compl of O & f is involutive );
end;

:: deftheorem Def6 defines Dneg OPOSET_1:def 6 :
for O being non empty OrthoRelStr holds
( O is Dneg iff ex f being Function of O,O st
( f = the Compl of O & f is involutive ) );

theorem :: OPOSET_1:20
canceled;

registration
cluster TrivOrthoRelStr -> strict Dneg ;
coherence
TrivOrthoRelStr is Dneg by Def6;
end;

registration
cluster non empty Dneg OrthoRelStr ;
existence
ex b1 being non empty OrthoRelStr st b1 is Dneg by Def4;
end;

definition
let O be non empty RelStr ;
canceled;
canceled;
attr O is SubReFlexive means :Def9: :: OPOSET_1:def 9
 the InternalRel of O is reflexive ;
end;

:: deftheorem OPOSET_1:def 7 :
canceled;

:: deftheorem OPOSET_1:def 8 :
canceled;

:: deftheorem Def9 defines SubReFlexive OPOSET_1:def 9 :
for O being non empty RelStr holds
( O is SubReFlexive iff the InternalRel of O is reflexive );

theorem :: OPOSET_1:21
for O being non empty RelStr st O is reflexive holds
O is SubReFlexive
proof end;

theorem Th22: :: OPOSET_1:22
TrivOrthoRelStr is reflexive
proof end;

registration
cluster TrivOrthoRelStr -> reflexive strict ;
coherence
TrivOrthoRelStr is reflexive by Th22;
end;

registration
cluster non empty reflexive strict OrthoRelStr ;
existence
ex b1 being non empty OrthoRelStr st
( b1 is reflexive & b1 is strict ) by Th22;
end;

definition
let O be non empty RelStr ;
canceled;
redefine attr O is irreflexive means :Def11: :: OPOSET_1:def 11
 the InternalRel of O is irreflexive ;
compatibility
( O is irreflexive iff the InternalRel of O is irreflexive )
proof end;
redefine attr O is irreflexive means :Def12: :: OPOSET_1:def 12
 the InternalRel of O is_irreflexive_in the carrier of O;
compatibility
( O is irreflexive iff the InternalRel of O is_irreflexive_in the carrier of O )
proof end;
end;

:: deftheorem OPOSET_1:def 10 :
canceled;

:: deftheorem Def11 defines irreflexive OPOSET_1:def 11 :
for O being non empty RelStr holds
( O is irreflexive iff the InternalRel of O is irreflexive );

:: deftheorem Def12 defines irreflexive OPOSET_1:def 12 :
for O being non empty RelStr holds
( O is irreflexive iff the InternalRel of O is_irreflexive_in the carrier of O );

theorem :: OPOSET_1:23
canceled;

theorem Th24: :: OPOSET_1:24
TrivAsymOrthoRelStr is irreflexive
proof end;

registration
cluster TrivAsymOrthoRelStr -> irreflexive strict ;
coherence
TrivAsymOrthoRelStr is irreflexive by Th24;
end;

registration
cluster non empty irreflexive strict OrthoRelStr ;
existence
ex b1 being non empty OrthoRelStr st
( b1 is irreflexive & b1 is strict ) by Th24;
end;

definition
let O be non empty RelStr ;
redefine attr O is symmetric means :Def13: :: OPOSET_1:def 13
 the InternalRel of O is symmetric Relation of the carrier of O;
compatibility
( O is symmetric iff the InternalRel of O is symmetric Relation of the carrier of O )
proof end;
end;

:: deftheorem Def13 defines symmetric OPOSET_1:def 13 :
for O being non empty RelStr holds
( O is symmetric iff the InternalRel of O is symmetric Relation of the carrier of O );

theorem :: OPOSET_1:25
canceled;

theorem Th26: :: OPOSET_1:26
TrivOrthoRelStr is symmetric
proof end;

registration
cluster non empty symmetric strict OrthoRelStr ;
existence
ex b1 being non empty OrthoRelStr st
( b1 is symmetric & b1 is strict ) by Th26;
end;

definition
let O be non empty RelStr ;
canceled;
redefine attr O is antisymmetric means :: OPOSET_1:def 15
 the InternalRel of O is antisymmetric Relation of the carrier of O;
compatibility
( O is antisymmetric iff the InternalRel of O is antisymmetric Relation of the carrier of O )
proof end;
end;

:: deftheorem OPOSET_1:def 14 :
canceled;

:: deftheorem defines antisymmetric OPOSET_1:def 15 :
for O being non empty RelStr holds
( O is antisymmetric iff the InternalRel of O is antisymmetric Relation of the carrier of O );

theorem :: OPOSET_1:27
canceled;

Lm1: TrivOrthoRelStr is antisymmetric
;

registration
cluster TrivOrthoRelStr -> symmetric strict ;
coherence
TrivOrthoRelStr is symmetric by Th26;
end;

registration
cluster non empty antisymmetric symmetric strict OrthoRelStr ;
existence
ex b1 being non empty OrthoRelStr st
( b1 is symmetric & b1 is antisymmetric & b1 is strict ) by Lm1;
end;

definition
let O be non empty RelStr ;
canceled;
canceled;
redefine attr O is asymmetric means :Def18: :: OPOSET_1:def 18
 the InternalRel of O is_asymmetric_in the carrier of O;
compatibility
( O is asymmetric iff the InternalRel of O is_asymmetric_in the carrier of O )
proof end;
end;

:: deftheorem OPOSET_1:def 16 :
canceled;

:: deftheorem OPOSET_1:def 17 :
canceled;

:: deftheorem Def18 defines asymmetric OPOSET_1:def 18 :
for O being non empty RelStr holds
( O is asymmetric iff the InternalRel of O is_asymmetric_in the carrier of O );

theorem :: OPOSET_1:28
canceled;

theorem :: OPOSET_1:29
canceled;

theorem Th30: :: OPOSET_1:30
TrivAsymOrthoRelStr is asymmetric
proof end;

registration
cluster TrivAsymOrthoRelStr -> asymmetric strict ;
coherence
TrivAsymOrthoRelStr is asymmetric by Th30;
end;

registration
cluster non empty asymmetric strict OrthoRelStr ;
existence
ex b1 being non empty OrthoRelStr st
( b1 is asymmetric & b1 is strict ) by Th30;
end;

definition
let O be non empty RelStr ;
redefine attr O is transitive means :Def19: :: OPOSET_1:def 19
 the InternalRel of O is transitive Relation of the carrier of O;
compatibility
( O is transitive iff the InternalRel of O is transitive Relation of the carrier of O )
proof end;
end;

:: deftheorem Def19 defines transitive OPOSET_1:def 19 :
for O being non empty RelStr holds
( O is transitive iff the InternalRel of O is transitive Relation of the carrier of O );

theorem :: OPOSET_1:31
canceled;

registration
cluster non empty reflexive transitive antisymmetric symmetric strict OrthoRelStr ;
existence
ex b1 being non empty OrthoRelStr st
( b1 is reflexive & b1 is symmetric & b1 is antisymmetric & b1 is transitive & b1 is strict ) by Lm1;
end;

theorem :: OPOSET_1:32
canceled;

theorem Th33: :: OPOSET_1:33
TrivAsymOrthoRelStr is transitive
proof end;

registration
cluster TrivAsymOrthoRelStr -> transitive asymmetric irreflexive strict ;
coherence
( TrivAsymOrthoRelStr is irreflexive & TrivAsymOrthoRelStr is asymmetric & TrivAsymOrthoRelStr is transitive ) by Th33;
end;

registration
cluster non empty transitive asymmetric irreflexive strict OrthoRelStr ;
existence
ex b1 being non empty OrthoRelStr st
( b1 is irreflexive & b1 is asymmetric & b1 is transitive & b1 is strict ) by Th24;
end;

theorem :: OPOSET_1:34
for O being non empty RelStr st O is symmetric & O is transitive holds
O is SubReFlexive
proof end;

theorem :: OPOSET_1:35
for O being non empty RelStr st O is irreflexive & O is transitive holds
O is asymmetric
proof end;

theorem Th36: :: OPOSET_1:36
for O being non empty RelStr st O is asymmetric holds
O is irreflexive
proof end;

theorem :: OPOSET_1:37
canceled;

theorem :: OPOSET_1:38
canceled;

theorem :: OPOSET_1:39
canceled;

theorem :: OPOSET_1:40
canceled;

theorem :: OPOSET_1:41
canceled;

begin

definition
let O be non empty RelStr ;
canceled;
attr O is SubQuasiOrdered means :Def21: :: OPOSET_1:def 21
( O is SubReFlexive & O is transitive );
end;

:: deftheorem OPOSET_1:def 20 :
canceled;

:: deftheorem Def21 defines SubQuasiOrdered OPOSET_1:def 21 :
for O being non empty RelStr holds
( O is SubQuasiOrdered iff ( O is SubReFlexive & O is transitive ) );

notation
let O be non empty RelStr ;
synonym SubPreOrdered O for SubQuasiOrdered ;
end;

definition
let O be non empty RelStr ;
attr O is QuasiOrdered means :Def22: :: OPOSET_1:def 22
( O is reflexive & O is transitive );
end;

:: deftheorem Def22 defines QuasiOrdered OPOSET_1:def 22 :
for O being non empty RelStr holds
( O is QuasiOrdered iff ( O is reflexive & O is transitive ) );

notation
let O be non empty RelStr ;
synonym PreOrdered O for QuasiOrdered ;
end;

theorem Th42: :: OPOSET_1:42
for O being non empty RelStr st O is QuasiOrdered holds
O is SubQuasiOrdered
proof end;

registration
cluster non empty QuasiOrdered -> non empty SubQuasiOrdered OrthoRelStr ;
correctness
coherence
for b1 being non empty OrthoRelStr st b1 is QuasiOrdered holds
b1 is SubQuasiOrdered ;
by Th42;
end;

registration
cluster TrivOrthoRelStr -> strict QuasiOrdered ;
coherence
TrivOrthoRelStr is QuasiOrdered by Def22;
end;

definition
let O be non empty OrthoRelStr ;
attr O is QuasiPure means :Def23: :: OPOSET_1:def 23
( O is Dneg & O is QuasiOrdered );
end;

:: deftheorem Def23 defines QuasiPure OPOSET_1:def 23 :
for O being non empty OrthoRelStr holds
( O is QuasiPure iff ( O is Dneg & O is QuasiOrdered ) );

registration
cluster non empty strict Dneg QuasiOrdered QuasiPure OrthoRelStr ;
existence
ex b1 being non empty OrthoRelStr st
( b1 is QuasiPure & b1 is Dneg & b1 is QuasiOrdered & b1 is strict )
proof end;
end;

registration
cluster TrivOrthoRelStr -> strict QuasiPure ;
coherence
TrivOrthoRelStr is QuasiPure by Def23;
end;

definition
mode QuasiPureOrthoRelStr is non empty QuasiPure OrthoRelStr ;
end;

definition
canceled;
let O be non empty OrthoRelStr ;
attr O is PartialOrdered means :Def25: :: OPOSET_1:def 25
( O is reflexive & O is antisymmetric & O is transitive );
end;

:: deftheorem OPOSET_1:def 24 :
canceled;

:: deftheorem Def25 defines PartialOrdered OPOSET_1:def 25 :
for O being non empty OrthoRelStr holds
( O is PartialOrdered iff ( O is reflexive & O is antisymmetric & O is transitive ) );

theorem :: OPOSET_1:43
canceled;

registration
cluster non empty PartialOrdered -> non empty reflexive transitive antisymmetric OrthoRelStr ;
coherence
for b1 being non empty OrthoRelStr st b1 is PartialOrdered holds
( b1 is reflexive & b1 is antisymmetric & b1 is transitive ) by Def25;
cluster non empty reflexive transitive antisymmetric -> non empty PartialOrdered OrthoRelStr ;
coherence
for b1 being non empty OrthoRelStr st b1 is reflexive & b1 is antisymmetric & b1 is transitive holds
b1 is PartialOrdered by Def25;
end;

definition
let O be non empty OrthoRelStr ;
attr O is Pure means :Def26: :: OPOSET_1:def 26
( O is Dneg & O is PartialOrdered );
end;

:: deftheorem Def26 defines Pure OPOSET_1:def 26 :
for O being non empty OrthoRelStr holds
( O is Pure iff ( O is Dneg & O is PartialOrdered ) );

registration
cluster non empty strict Dneg PartialOrdered Pure OrthoRelStr ;
existence
ex b1 being non empty OrthoRelStr st
( b1 is Pure & b1 is Dneg & b1 is PartialOrdered & b1 is strict )
proof end;
end;

registration
cluster TrivOrthoRelStr -> strict Pure ;
coherence
TrivOrthoRelStr is Pure by Def26;
end;

definition
mode PureOrthoRelStr is non empty Pure OrthoRelStr ;
end;

definition
canceled;
let O be non empty OrthoRelStr ;
attr O is StrictPartialOrdered means :Def28: :: OPOSET_1:def 28
( O is asymmetric & O is transitive );
end;

:: deftheorem OPOSET_1:def 27 :
canceled;

:: deftheorem Def28 defines StrictPartialOrdered OPOSET_1:def 28 :
for O being non empty OrthoRelStr holds
( O is StrictPartialOrdered iff ( O is asymmetric & O is transitive ) );

notation
let O be non empty OrthoRelStr ;
synonym StrictOrdered O for StrictPartialOrdered ;
end;

theorem :: OPOSET_1:44
canceled;

theorem Th45: :: OPOSET_1:45
for O being non empty OrthoRelStr st O is StrictPartialOrdered holds
O is irreflexive
proof end;

registration
cluster non empty StrictPartialOrdered -> non empty irreflexive OrthoRelStr ;
coherence
for b1 being non empty OrthoRelStr st b1 is StrictPartialOrdered holds
b1 is irreflexive by Th45;
end;

theorem :: OPOSET_1:46
canceled;

theorem :: OPOSET_1:47
canceled;

registration
cluster non empty StrictPartialOrdered -> non empty irreflexive OrthoRelStr ;
coherence
for b1 being non empty OrthoRelStr st b1 is StrictPartialOrdered holds
b1 is irreflexive ;
end;

registration
cluster TrivAsymOrthoRelStr -> irreflexive strict StrictPartialOrdered ;
coherence
( TrivAsymOrthoRelStr is irreflexive & TrivAsymOrthoRelStr is StrictPartialOrdered ) by Def28;
end;

registration
cluster non empty irreflexive strict StrictPartialOrdered OrthoRelStr ;
existence
ex b1 being non empty strict OrthoRelStr st
( b1 is irreflexive & b1 is StrictPartialOrdered )
proof end;
end;

theorem :: OPOSET_1:48
for QO being non empty QuasiOrdered OrthoRelStr st QO is antisymmetric holds
QO is PartialOrdered
proof end;

registration
cluster non empty PartialOrdered -> non empty reflexive transitive antisymmetric OrthoRelStr ;
correctness
coherence
for b1 being non empty OrthoRelStr st b1 is PartialOrdered holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric );
;
end;

definition
let PO be non empty RelStr ;
let f be UnOp of the carrier of PO;
canceled;
canceled;
canceled;
attr f is Orderinvolutive means :Def32: :: OPOSET_1:def 32
 ex g being Function of PO,PO st
( g = f & g is involutive & g is antitone );
end;

:: deftheorem OPOSET_1:def 29 :
canceled;

:: deftheorem OPOSET_1:def 30 :
canceled;

:: deftheorem OPOSET_1:def 31 :
canceled;

:: deftheorem Def32 defines Orderinvolutive OPOSET_1:def 32 :
for PO being non empty RelStr
for f being UnOp of the carrier of PO holds
( f is Orderinvolutive iff ex g being Function of PO,PO st
( g = f & g is involutive & g is antitone ) );

definition
let PO be non empty OrthoRelStr ;
attr PO is OrderInvolutive means :Def33: :: OPOSET_1:def 33
 ex f being Function of PO,PO st
( f = the Compl of PO & f is Orderinvolutive );
end;

:: deftheorem Def33 defines OrderInvolutive OPOSET_1:def 33 :
for PO being non empty OrthoRelStr holds
( PO is OrderInvolutive iff ex f being Function of PO,PO st
( f = the Compl of PO & f is Orderinvolutive ) );

theorem :: OPOSET_1:49
canceled;

theorem Th50: :: OPOSET_1:50
the Compl of TrivOrthoRelStr is Orderinvolutive
proof end;

registration
cluster TrivOrthoRelStr -> strict OrderInvolutive ;
coherence
TrivOrthoRelStr is OrderInvolutive by Def33, Th50;
end;

registration
cluster non empty PartialOrdered Pure OrderInvolutive OrthoRelStr ;
existence
ex b1 being non empty OrthoRelStr st
( b1 is OrderInvolutive & b1 is Pure & b1 is PartialOrdered )
proof end;
end;

definition
mode PreOrthoPoset is non empty PartialOrdered Pure OrderInvolutive OrthoRelStr ;
end;

definition
let PO be non empty RelStr ;
let f be UnOp of the carrier of PO;
pred f QuasiOrthoComplement_on PO means :Def34: :: OPOSET_1:def 34
( f is Orderinvolutive & ( for y being Element of PO holds
( ex_sup_of {y,(f . y)},PO & ex_inf_of {y,(f . y)},PO ) ) );
end;

:: deftheorem Def34 defines QuasiOrthoComplement_on OPOSET_1:def 34 :
for PO being non empty RelStr
for f being UnOp of the carrier of PO holds
( f QuasiOrthoComplement_on PO iff ( f is Orderinvolutive & ( for y being Element of PO holds
( ex_sup_of {y,(f . y)},PO & ex_inf_of {y,(f . y)},PO ) ) ) );

definition
let PO be non empty OrthoRelStr ;
attr PO is QuasiOrthocomplemented means :Def35: :: OPOSET_1:def 35
 ex f being Function of PO,PO st
( f = the Compl of PO & f QuasiOrthoComplement_on PO );
end;

:: deftheorem Def35 defines QuasiOrthocomplemented OPOSET_1:def 35 :
for PO being non empty OrthoRelStr holds
( PO is QuasiOrthocomplemented iff ex f being Function of PO,PO st
( f = the Compl of PO & f QuasiOrthoComplement_on PO ) );

Lm2: id {{}} = {[{},{}]}
by SYSREL:30;

theorem Th51: :: OPOSET_1:51
TrivOrthoRelStr is QuasiOrthocomplemented
proof end;

definition
let PO be non empty RelStr ;
let f be UnOp of the carrier of PO;
pred f OrthoComplement_on PO means :Def36: :: OPOSET_1:def 36
( f is Orderinvolutive & ( for y being Element of PO holds
( ex_sup_of {y,(f . y)},PO & ex_inf_of {y,(f . y)},PO & "\/" ({y,(f . y)},PO) is_maximum_of the carrier of PO & "/\" ({y,(f . y)},PO) is_minimum_of the carrier of PO ) ) );
end;

:: deftheorem Def36 defines OrthoComplement_on OPOSET_1:def 36 :
for PO being non empty RelStr
for f being UnOp of the carrier of PO holds
( f OrthoComplement_on PO iff ( f is Orderinvolutive & ( for y being Element of PO holds
( ex_sup_of {y,(f . y)},PO & ex_inf_of {y,(f . y)},PO & "\/" ({y,(f . y)},PO) is_maximum_of the carrier of PO & "/\" ({y,(f . y)},PO) is_minimum_of the carrier of PO ) ) ) );

definition
let PO be non empty OrthoRelStr ;
attr PO is Orthocomplemented means :Def37: :: OPOSET_1:def 37
 ex f being Function of PO,PO st
( f = the Compl of PO & f OrthoComplement_on PO );
end;

:: deftheorem Def37 defines Orthocomplemented OPOSET_1:def 37 :
for PO being non empty OrthoRelStr holds
( PO is Orthocomplemented iff ex f being Function of PO,PO st
( f = the Compl of PO & f OrthoComplement_on PO ) );

theorem :: OPOSET_1:52
for PO being non empty OrthoRelStr
for f being UnOp of the carrier of PO st f OrthoComplement_on PO holds
f QuasiOrthoComplement_on PO
proof end;

theorem Th53: :: OPOSET_1:53
TrivOrthoRelStr is Orthocomplemented
proof end;

registration
cluster TrivOrthoRelStr -> strict QuasiOrthocomplemented Orthocomplemented ;
coherence
( TrivOrthoRelStr is QuasiOrthocomplemented & TrivOrthoRelStr is Orthocomplemented ) by Th51, Th53;
end;

registration
cluster non empty PartialOrdered QuasiOrthocomplemented Orthocomplemented OrthoRelStr ;
correctness
existence
ex b1 being non empty OrthoRelStr st
( b1 is Orthocomplemented & b1 is QuasiOrthocomplemented & b1 is PartialOrdered );
proof end;
end;

definition
mode QuasiOrthoPoset is non empty PartialOrdered QuasiOrthocomplemented OrthoRelStr ;
mode OrthoPoset is non empty PartialOrdered Orthocomplemented OrthoRelStr ;
end;