oposet_1.miz

    begin

    reserve X for non empty set,

R for Relation of X;

    theorem :: OPOSET_1:1

    for L be non empty reflexive antisymmetric RelStr holds for x,y be Element of L holds x <= y implies ( sup {x, y}) = y & ( inf {x, y}) = x

    proof

      let R be non empty reflexive antisymmetric RelStr;

      let a,b be Element of R;



       A1: for x be Element of R st x is_>=_than {a, b} holds b <= x

      proof

        let a0 be Element of R;



         A2: b in {a, b} by TARSKI:def 2;

        assume a0 is_>=_than {a, b};

        hence thesis by A2, LATTICE3:def 9;

      end;



       A3: for x be Element of R st x is_<=_than {a, b} holds a >= x

      proof

        let a0 be Element of R;



         A4: a in {a, b} by TARSKI:def 2;

        assume a0 is_<=_than {a, b};

        hence thesis by A4, LATTICE3:def 8;

      end;

      assume

       A5: a <= b;

      for x be Element of {a, b} holds x >= a

      proof

        let a0 be Element of {a, b};

        a <= a0 or a <= a0 by A5, TARSKI:def 2;

        hence thesis;

      end;

      then for x be Element of R st x in {a, b} holds x >= a;

      then

       A6: a is_<=_than {a, b} by LATTICE3:def 8;

      for x be Element of R st x in {a, b} holds x <= b by A5, TARSKI:def 2;

      then b is_>=_than {a, b} by LATTICE3:def 9;

      hence thesis by A6, A1, A3, YELLOW_0: 30, YELLOW_0: 31;

    end;

    registration

      let X be set;

      cluster irreflexive asymmetric transitive for Relation of X;

      existence

      proof

        ( {} (X,X)) = {} ;

        hence thesis;

      end;

    end

    registration

      let X, R;

      let C be UnOp of X;

      cluster OrthoRelStr (# X, R, C #) -> non empty;

      coherence ;

    end

    registration

      cluster non empty strict for OrthoRelStr;

      existence

      proof

        set X = the non empty set, R = the Relation of X, C = the UnOp of X;

        take OrthoRelStr (# X, R, C #);

        thus thesis;

      end;

    end

    registration

      let O be set;

      cluster involutive for Function of O, O;

      existence

      proof

        take ( id O);

        thus thesis;

      end;

    end

    definition

      :: OPOSET_1:def1

      func TrivOrthoRelStr -> strict OrthoRelStr equals

      : Def1: OrthoRelStr (# { 0 }, ( id { 0 }), op1 #);

      coherence ;

    end

    notation

      synonym TrivPoset for TrivOrthoRelStr ;

    end

    registration

      cluster TrivOrthoRelStr -> 1 -element;

      coherence ;

    end

    definition

      :: OPOSET_1:def2

      func TrivAsymOrthoRelStr -> strict OrthoRelStr equals OrthoRelStr (# { 0 }, ( {} ( { 0 }, { 0 })), op1 #);

      coherence ;

    end

    registration

      cluster TrivAsymOrthoRelStr -> non empty;

      coherence ;

    end

    definition

      let O be non empty OrthoRelStr;

      :: OPOSET_1:def3

      attr O is Dneg means ex f be Function of O, O st f = the Compl of O & f is involutive;

    end

    registration

      cluster TrivOrthoRelStr -> Dneg;

      coherence ;

    end

    registration

      cluster Dneg for non empty OrthoRelStr;

      existence by Def1;

    end

    definition

      let O be non empty RelStr;

      :: OPOSET_1:def4

      attr O is SubReFlexive means

      : Def4: the InternalRel of O is reflexive;

    end

    reserve O for non empty RelStr;

    theorem :: OPOSET_1:2

    O is reflexive implies O is SubReFlexive by PARTIT_2: 21;

    theorem :: OPOSET_1:3



     Th3: TrivOrthoRelStr is reflexive

    proof

      ( rng ( id { {} })) = { {} } & ( field ( id { {} })) = (( dom ( id { {} })) \/ ( rng ( id { {} })));

      hence thesis by RELAT_2:def 9;

    end;

    registration

      cluster TrivOrthoRelStr -> reflexive;

      coherence by Th3;

    end

    registration

      cluster reflexive strict for non empty OrthoRelStr;

      existence by Th3;

    end

    definition

      let O;

      :: original: irreflexive

      redefine

      :: OPOSET_1:def5

      attr O is irreflexive means the InternalRel of O is irreflexive;

      compatibility

      proof

        set RO = the InternalRel of O;



         A1: ( field RO) c= (the carrier of O \/ the carrier of O) by RELSET_1: 8;

        thus O is irreflexive implies RO is irreflexive

        proof

          assume

           A2: O is irreflexive;

          let x be object;

          thus thesis by A1, A2;

        end;

        assume

         A3: RO is_irreflexive_in ( field RO);

        let x be set;

        assume x in the carrier of O;

        per cases ;

          suppose x in ( field RO);

          hence not [x, x] in RO by A3;

        end;

          suppose not x in ( field RO);

          hence not [x, x] in RO by RELAT_1: 15;

        end;

      end;

      :: original: irreflexive

      redefine

      :: OPOSET_1:def6

      attr O is irreflexive means the InternalRel of O is_irreflexive_in the carrier of O;

      compatibility ;

    end

    theorem :: OPOSET_1:4



     Th4: TrivAsymOrthoRelStr is irreflexive;

    registration

      cluster TrivAsymOrthoRelStr -> irreflexive;

      coherence ;

    end

    registration

      cluster irreflexive strict for non empty OrthoRelStr;

      existence by Th4;

    end

    definition

      let O be non empty RelStr;

      :: original: symmetric

      redefine

      :: OPOSET_1:def7

      attr O is symmetric means the InternalRel of O is symmetric Relation of the carrier of O;

      compatibility by PARTIT_2: 22, PARTIT_2: 23;

    end

    theorem :: OPOSET_1:5



     Th5: TrivOrthoRelStr is symmetric;

    registration

      cluster symmetric strict for non empty OrthoRelStr;

      existence by Th5;

    end

    definition

      let O;

      :: original: antisymmetric

      redefine

      :: OPOSET_1:def8

      attr O is antisymmetric means the InternalRel of O is antisymmetric Relation of the carrier of O;

      compatibility by PARTIT_2: 25, PARTIT_2: 24;

    end



     Lm1: TrivOrthoRelStr is antisymmetric;

    registration

      cluster TrivOrthoRelStr -> symmetric;

      coherence ;

    end

    registration

      cluster symmetric antisymmetric strict for non empty OrthoRelStr;

      existence by Lm1;

    end

    definition

      let O;

      :: original: asymmetric

      redefine

      :: OPOSET_1:def9

      attr O is asymmetric means the InternalRel of O is_asymmetric_in the carrier of O;

      compatibility by PARTIT_2: 28, PARTIT_2: 29;

    end

    theorem :: OPOSET_1:6



     Th6: TrivAsymOrthoRelStr is asymmetric;

    registration

      cluster TrivAsymOrthoRelStr -> asymmetric;

      coherence ;

    end

    registration

      cluster asymmetric strict for non empty OrthoRelStr;

      existence by Th6;

    end

    definition

      let O;

      :: original: transitive

      redefine

      :: OPOSET_1:def10

      attr O is transitive means the InternalRel of O is transitive Relation of the carrier of O;

      compatibility by PARTIT_2: 27, PARTIT_2: 26;

    end

    registration

      cluster reflexive symmetric antisymmetric transitive strict for non empty OrthoRelStr;

      existence by Lm1;

    end

    theorem :: OPOSET_1:7

     TrivAsymOrthoRelStr is transitive;

    registration

      cluster TrivAsymOrthoRelStr -> irreflexive asymmetric transitive;

      coherence ;

    end

    registration

      cluster irreflexive asymmetric transitive strict for non empty OrthoRelStr;

      existence by Th4;

    end

    theorem :: OPOSET_1:8

    O is symmetric transitive implies O is SubReFlexive;

    theorem :: OPOSET_1:9

    O is irreflexive transitive implies O is asymmetric;

    theorem :: OPOSET_1:10

    O is asymmetric implies O is irreflexive;

    begin

    definition

      let O;

      :: OPOSET_1:def11

      attr O is SubQuasiOrdered means O is SubReFlexive transitive;

    end

    notation

      let O;

      synonym O is SubPreOrdered for O is SubQuasiOrdered;

    end

    definition

      let O;

      :: OPOSET_1:def12

      attr O is QuasiOrdered means

      : Def12: O is reflexive transitive;

    end

    notation

      let O;

      synonym O is PreOrdered for O is QuasiOrdered;

    end

    theorem :: OPOSET_1:11



     Th11: O is QuasiOrdered implies O is SubQuasiOrdered

    proof

      set IntRel = the InternalRel of O;

      set CO = the carrier of O;

      assume

       A1: O is QuasiOrdered;

      then

       A2: O is transitive;

      O is reflexive by A1;

      then IntRel is_reflexive_in CO;

      then IntRel is reflexive by PARTIT_2: 21;

      hence thesis by A2, Def4;

    end;

    registration

      cluster QuasiOrdered -> SubQuasiOrdered for non empty OrthoRelStr;

      correctness by Th11;

    end

    registration

      cluster TrivOrthoRelStr -> QuasiOrdered;

      coherence ;

    end

    reserve O for non empty OrthoRelStr;

    definition

      let O;

      :: OPOSET_1:def13

      attr O is QuasiPure means O is Dneg QuasiOrdered;

    end

    registration

      cluster QuasiPure Dneg QuasiOrdered strict for non empty OrthoRelStr;

      existence

      proof

         TrivOrthoRelStr is QuasiPure;

        hence thesis;

      end;

    end

    registration

      cluster TrivOrthoRelStr -> QuasiPure;

      coherence ;

    end

    definition

      mode QuasiPureOrthoRelStr is QuasiPure non empty OrthoRelStr;

    end

    definition

      let O;

      :: OPOSET_1:def14

      attr O is PartialOrdered means O is reflexive antisymmetric transitive;

    end

    registration

      cluster PartialOrdered -> reflexive antisymmetric transitive for non empty OrthoRelStr;

      coherence ;

      cluster reflexive antisymmetric transitive -> PartialOrdered for non empty OrthoRelStr;

      coherence ;

    end

    definition

      let O;

      :: OPOSET_1:def15

      attr O is Pure means O is Dneg PartialOrdered;

    end

    registration

      cluster Pure Dneg PartialOrdered strict for non empty OrthoRelStr;

      existence

      proof

         TrivOrthoRelStr is Pure;

        hence thesis;

      end;

    end

    registration

      cluster TrivOrthoRelStr -> Pure;

      coherence ;

    end

    definition

      mode PureOrthoRelStr is Pure non empty OrthoRelStr;

    end

    definition

      let O;

      :: OPOSET_1:def16

      attr O is StrictPartialOrdered means O is asymmetric transitive;

    end

    notation

      let O;

      synonym O is StrictOrdered for O is StrictPartialOrdered;

    end

    theorem :: OPOSET_1:12



     Th12: O is StrictPartialOrdered implies O is irreflexive

    proof

      assume O is StrictPartialOrdered;

      then O is asymmetric transitive;

      hence thesis;

    end;

    registration

      cluster StrictPartialOrdered -> irreflexive for non empty OrthoRelStr;

      coherence by Th12;

    end

    registration

      cluster StrictPartialOrdered -> irreflexive for non empty OrthoRelStr;

      coherence ;

    end

    registration

      cluster TrivAsymOrthoRelStr -> irreflexive StrictPartialOrdered;

      coherence ;

    end

    registration

      cluster irreflexive StrictPartialOrdered for non empty strict OrthoRelStr;

      existence

      proof

         TrivAsymOrthoRelStr is StrictPartialOrdered;

        hence thesis;

      end;

    end

    reserve QO for QuasiOrdered non empty OrthoRelStr;

    theorem :: OPOSET_1:13

    QO is antisymmetric implies QO is PartialOrdered by Def12;

    registration

      cluster PartialOrdered -> reflexive transitive antisymmetric for non empty OrthoRelStr;

      correctness ;

    end

    definition

      let PO be non empty RelStr;

      let f be UnOp of the carrier of PO;

      :: OPOSET_1:def17

      attr f is Orderinvolutive means f is involutive antitone;

    end

    definition

      let PO be non empty OrthoRelStr;

      :: OPOSET_1:def18

      attr PO is OrderInvolutive means the Compl of PO is Orderinvolutive;

    end

    theorem :: OPOSET_1:14



     Th14: the Compl of TrivOrthoRelStr is Orderinvolutive

    proof

      set O = TrivOrthoRelStr ;

      set C = the Compl of O;

      reconsider Emp = {} as Element of O by TARSKI:def 1;

      C is antitone Function of O, O

      proof

        reconsider f = C as Function of O, O;

        for x1,x2 be Element of O st x1 <= x2 holds for y1,y2 be Element of O st y1 = (f . x1) & y2 = (f . x2) holds y1 >= y2

        proof

          let a1,a2 be Element of O;

          set b1 = (f . a1);

          b1 = Emp by FUNCT_2: 50;

          then (f . a2) <= b1 by FUNCT_2: 50;

          hence thesis;

        end;

        hence thesis by WAYBEL_0:def 5;

      end;

      hence thesis;

    end;

    registration

      cluster TrivOrthoRelStr -> OrderInvolutive;

      coherence by Th14;

    end

    registration

      cluster OrderInvolutive Pure PartialOrdered for non empty OrthoRelStr;

      existence

      proof

        take TrivOrthoRelStr ;

        thus thesis;

      end;

    end

    definition

      mode PreOrthoPoset is OrderInvolutive Pure PartialOrdered non empty OrthoRelStr;

    end

    definition

      let PO be non empty RelStr;

      let f be UnOp of the carrier of PO;

      :: OPOSET_1:def19

      pred f QuasiOrthoComplement_on PO means f is Orderinvolutive & for y be Element of PO holds ex_sup_of ( {y, (f . y)},PO) & ex_inf_of ( {y, (f . y)},PO);

    end

    definition

      let PO be non empty OrthoRelStr;

      :: OPOSET_1:def20

      attr PO is QuasiOrthocomplemented means ex f be Function of PO, PO st f = the Compl of PO & f QuasiOrthoComplement_on PO;

    end



     Lm2: ( id { {} }) = { [ {} , {} ]} by SYSREL: 13;

    theorem :: OPOSET_1:15



     Th15: TrivOrthoRelStr is QuasiOrthocomplemented

    proof

      set O = TrivOrthoRelStr ;

      set C = the Compl of O;

      set S = the carrier of O;

      C QuasiOrthoComplement_on O

      proof

        reconsider f = C as Function of O, O;



         A1: for x be Element of S holds {x, ( op1 . x)} = {x} by Lm2, PARTIT_2: 19, ENUMSET1: 29;

        for x be Element of O holds ( sup {x, (f . x)}) = x & ( inf {x, (f . x)}) = x & ex_sup_of ( {x, (f . x)},O) & ex_inf_of ( {x, (f . x)},O)

        proof

          let a be Element of O;

           {a, (f . a)} = {a} by A1;

          hence thesis by YELLOW_0: 38, YELLOW_0: 39;

        end;

        hence thesis by Th14;

      end;

      hence thesis;

    end;

    definition

      let PO be non empty RelStr;

      let f be UnOp of the carrier of PO;

      :: OPOSET_1:def21

      pred f OrthoComplement_on PO means f is Orderinvolutive & for y be 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

    definition

      let PO be non empty OrthoRelStr;

      :: OPOSET_1:def22

      attr PO is Orthocomplemented means ex f be Function of PO, PO st f = the Compl of PO & f OrthoComplement_on PO;

    end

    theorem :: OPOSET_1:16

    for PO be non empty OrthoRelStr, f be UnOp of the carrier of PO st f OrthoComplement_on PO holds f QuasiOrthoComplement_on PO;

    theorem :: OPOSET_1:17



     Th17: TrivOrthoRelStr is Orthocomplemented

    proof

      set O = TrivOrthoRelStr ;

      set C = the Compl of O;

      set S = the carrier of O;

      reconsider f = C as Function of O, O;

      f OrthoComplement_on O

      proof

        reconsider f = C as Function of O, O;



         A1: for x be Element of S holds {x, ( op1 . x)} = {x} by Lm2, PARTIT_2: 19, ENUMSET1: 29;



         A2: for x be Element of O holds ex_sup_of ( {x, (f . x)},O) & ex_inf_of ( {x, (f . x)},O) & ( sup {x, (f . x)}) = x & ( inf {x, (f . x)}) = x

        proof

          let a be Element of O;

           {a, (f . a)} = {a} by A1;

          hence thesis by YELLOW_0: 38, YELLOW_0: 39;

        end;



         A3: for x be Element of O holds ( sup {x, (f . x)}) in {x, (f . x)} & ( inf {x, (f . x)}) in {x, (f . x)}

        proof

          let a be Element of O;

          ( sup {a, (f . a)}) = a & ( inf {a, (f . a)}) = a by A2;

          hence thesis by TARSKI:def 2;

        end;



         A4: for x be Element of O holds x is_maximum_of {x, (f . x)} & x is_minimum_of {x, (f . x)}

        proof

          let a be Element of O;



           A5: ( sup {a, (f . a)}) = a & ex_sup_of ( {a, (f . a)},O) by A2;

          ( sup {a, (f . a)}) in {a, (f . a)} & ( inf {a, (f . a)}) = a by A2, A3;

          hence thesis by A5, A2, WAYBEL_1:def 6, WAYBEL_1:def 7;

        end;

        for y be Element of O holds ( sup {y, (f . y)}) is_maximum_of S & ( inf {y, (f . y)}) is_minimum_of S

        proof

          let a be Element of O;

          reconsider a0 = a as Element of S;

           {a0, (f . a0)} = {a0} by A1;

          then

           A6: {a0, (f . a0)} = S by TARSKI:def 1;

          a is_maximum_of {a, (f . a)} & a is_minimum_of {a, (f . a)} by A4;

          hence thesis by A2, A6;

        end;

        hence thesis by A2, Th14;

      end;

      hence thesis;

    end;

    registration

      cluster TrivOrthoRelStr -> QuasiOrthocomplemented Orthocomplemented;

      coherence by Th15, Th17;

    end

    registration

      cluster Orthocomplemented QuasiOrthocomplemented PartialOrdered for non empty OrthoRelStr;

      correctness

      proof

        take TrivOrthoRelStr ;

        thus thesis;

      end;

    end

    definition

      mode QuasiOrthoPoset is QuasiOrthocomplemented PartialOrdered non empty OrthoRelStr;

      mode OrthoPoset is Orthocomplemented PartialOrdered non empty OrthoRelStr;

    end