latsum_1.miz

    begin

    theorem :: LATSUM_1:1

    for x,y,A,B be set st x in (A \/ B) & y in (A \/ B) holds x in (A \ B) & y in (A \ B) or x in B & y in B or x in (A \ B) & y in B or x in B & y in (A \ B)

    proof

      let x,y,A,B be set;

      assume

       A1: x in (A \/ B) & y in (A \/ B);

      (A \/ B) = ((A \ B) \/ B) by XBOOLE_1: 39;

      hence thesis by A1, XBOOLE_0:def 3;

    end;

    definition

      let R,S be RelStr;

      :: LATSUM_1:def1

      pred R tolerates S means for x,y be set st x in (the carrier of R /\ the carrier of S) & y in (the carrier of R /\ the carrier of S) holds [x, y] in the InternalRel of R iff [x, y] in the InternalRel of S;

    end

    begin

    definition

      let R,S be RelStr;

      :: LATSUM_1:def2

      func R [*] S -> strict RelStr means

      : Def2: the carrier of it = (the carrier of R \/ the carrier of S) & the InternalRel of it = ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S));

      existence

      proof

        set X = (the carrier of R \/ the carrier of S);

        the carrier of R c= X & the carrier of S c= X by XBOOLE_1: 7;

        then

        reconsider G = (the InternalRel of R * the InternalRel of S) as Relation of X by RELSET_1: 7;

        the carrier of R c= X & the carrier of S c= X by XBOOLE_1: 7;

        then

        reconsider IR = the InternalRel of R, IS = the InternalRel of S as Relation of X by RELSET_1: 7;

        set F = ((IR \/ IS) \/ G);

        reconsider F as Relation of X;

        take RelStr (# X, F #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let R be RelStr, S be non empty RelStr;

      cluster (R [*] S) -> non empty;

      coherence

      proof

        (the carrier of R \/ the carrier of S) <> {} ;

        hence thesis by Def2;

      end;

    end

    registration

      let R be non empty RelStr, S be RelStr;

      cluster (R [*] S) -> non empty;

      coherence

      proof

        (the carrier of R \/ the carrier of S) <> {} ;

        hence thesis by Def2;

      end;

    end

    theorem :: LATSUM_1:2



     Th2: for R,S be RelStr holds the InternalRel of R c= the InternalRel of (R [*] S) & the InternalRel of S c= the InternalRel of (R [*] S)

    proof

      let R,S be RelStr;

      the InternalRel of R c= (the InternalRel of R \/ the InternalRel of S) & (the InternalRel of R \/ the InternalRel of S) c= ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by XBOOLE_1: 7;

      then the InternalRel of R c= ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by XBOOLE_1: 1;

      hence the InternalRel of R c= the InternalRel of (R [*] S) by Def2;

      the InternalRel of S c= (the InternalRel of R \/ the InternalRel of S) & (the InternalRel of R \/ the InternalRel of S) c= ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by XBOOLE_1: 7;

      then the InternalRel of S c= ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by XBOOLE_1: 1;

      hence thesis by Def2;

    end;

    theorem :: LATSUM_1:3



     Th3: for R,S be RelStr st R is reflexive & S is reflexive holds (R [*] S) is reflexive

    proof

      let R,S be RelStr;

      assume R is reflexive & S is reflexive;

      then

       A1: the InternalRel of R is_reflexive_in the carrier of R & the InternalRel of S is_reflexive_in the carrier of S by ORDERS_2:def 2;



       A2: the InternalRel of R c= the InternalRel of (R [*] S) & the InternalRel of S c= the InternalRel of (R [*] S) by Th2;

      the InternalRel of (R [*] S) is_reflexive_in the carrier of (R [*] S)

      proof

        let x be object;

        assume x in the carrier of (R [*] S);

        then x in (the carrier of R \/ the carrier of S) by Def2;

        then x in the carrier of R or x in the carrier of S by XBOOLE_0:def 3;

        then [x, x] in the InternalRel of R or [x, x] in the InternalRel of S by A1;

        hence thesis by A2;

      end;

      hence thesis by ORDERS_2:def 2;

    end;

    begin

    theorem :: LATSUM_1:4



     Th4: for R,S be RelStr, a,b be set st [a, b] in the InternalRel of (R [*] S) & a in the carrier of R & b in the carrier of R & R tolerates S & R is transitive holds [a, b] in the InternalRel of R

    proof

      let R,S be RelStr, a,b be set;

      assume that

       A1: [a, b] in the InternalRel of (R [*] S) and

       A2: a in the carrier of R and

       A3: b in the carrier of R and

       A4: R tolerates S and

       A5: R is transitive;

       [a, b] in ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by A1, Def2;

      then

       A6: [a, b] in (the InternalRel of R \/ the InternalRel of S) or [a, b] in (the InternalRel of R * the InternalRel of S) by XBOOLE_0:def 3;

      assume

       A7: not [a, b] in the InternalRel of R;

      per cases by A7, A6, XBOOLE_0:def 3;

        suppose

         A8: [a, b] in the InternalRel of S;

        then b in the carrier of S by ZFMISC_1: 87;

        then

         A9: b in (the carrier of R /\ the carrier of S) by A3, XBOOLE_0:def 4;

        a in the carrier of S by A8, ZFMISC_1: 87;

        then a in (the carrier of R /\ the carrier of S) by A2, XBOOLE_0:def 4;

        hence thesis by A4, A7, A8, A9;

      end;

        suppose

         A10: [a, b] in (the InternalRel of R * the InternalRel of S);

        then b in the carrier of S by ZFMISC_1: 87;

        then

         A11: b in (the carrier of R /\ the carrier of S) by A3, XBOOLE_0:def 4;



         A12: the InternalRel of R is_transitive_in the carrier of R by A5, ORDERS_2:def 3;

        consider z be object such that

         A13: [a, z] in the InternalRel of R and

         A14: [z, b] in the InternalRel of S by A10, RELAT_1:def 8;



         A15: z in the carrier of R by A13, ZFMISC_1: 87;

        z in the carrier of S by A14, ZFMISC_1: 87;

        then z in (the carrier of R /\ the carrier of S) by A15, XBOOLE_0:def 4;

        then [z, b] in the InternalRel of R by A4, A11, A14;

        hence thesis by A2, A3, A7, A13, A15, A12;

      end;

    end;

    theorem :: LATSUM_1:5



     Th5: for R,S be RelStr, a,b be set st [a, b] in the InternalRel of (R [*] S) & a in the carrier of S & b in the carrier of S & R tolerates S & S is transitive holds [a, b] in the InternalRel of S

    proof

      let R,S be RelStr, a,b be set;

      assume that

       A1: [a, b] in the InternalRel of (R [*] S) and

       A2: a in the carrier of S and

       A3: b in the carrier of S and

       A4: R tolerates S and

       A5: S is transitive;

       [a, b] in ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by A1, Def2;

      then

       A6: [a, b] in (the InternalRel of R \/ the InternalRel of S) or [a, b] in (the InternalRel of R * the InternalRel of S) by XBOOLE_0:def 3;

      assume

       A7: not [a, b] in the InternalRel of S;

      per cases by A7, A6, XBOOLE_0:def 3;

        suppose

         A8: [a, b] in the InternalRel of R;

        then b in the carrier of R by ZFMISC_1: 87;

        then

         A9: b in (the carrier of R /\ the carrier of S) by A3, XBOOLE_0:def 4;

        a in the carrier of R by A8, ZFMISC_1: 87;

        then a in (the carrier of R /\ the carrier of S) by A2, XBOOLE_0:def 4;

        hence thesis by A4, A7, A8, A9;

      end;

        suppose

         A10: [a, b] in (the InternalRel of R * the InternalRel of S);

        then a in the carrier of R by ZFMISC_1: 87;

        then

         A11: a in (the carrier of R /\ the carrier of S) by A2, XBOOLE_0:def 4;



         A12: the InternalRel of S is_transitive_in the carrier of S by A5, ORDERS_2:def 3;

        consider z be object such that

         A13: [a, z] in the InternalRel of R and

         A14: [z, b] in the InternalRel of S by A10, RELAT_1:def 8;



         A15: z in the carrier of S by A14, ZFMISC_1: 87;

        z in the carrier of R by A13, ZFMISC_1: 87;

        then z in (the carrier of R /\ the carrier of S) by A15, XBOOLE_0:def 4;

        then [a, z] in the InternalRel of S by A4, A11, A13;

        hence thesis by A2, A3, A7, A14, A15, A12;

      end;

    end;

    theorem :: LATSUM_1:6



     Th6: for R,S be RelStr, a,b be object holds ( [a, b] in the InternalRel of R implies [a, b] in the InternalRel of (R [*] S)) & ( [a, b] in the InternalRel of S implies [a, b] in the InternalRel of (R [*] S))

    proof

      let R,S be RelStr, a,b be object;

      thus [a, b] in the InternalRel of R implies [a, b] in the InternalRel of (R [*] S)

      proof

        assume [a, b] in the InternalRel of R;

        then [a, b] in (the InternalRel of R \/ the InternalRel of S) by XBOOLE_0:def 3;

        then [a, b] in ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by XBOOLE_0:def 3;

        hence thesis by Def2;

      end;

      assume [a, b] in the InternalRel of S;

      then [a, b] in (the InternalRel of R \/ the InternalRel of S) by XBOOLE_0:def 3;

      then [a, b] in ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by XBOOLE_0:def 3;

      hence thesis by Def2;

    end;

    theorem :: LATSUM_1:7

    for R,S be non empty RelStr, x be Element of (R [*] S) holds x in the carrier of R or x in (the carrier of S \ the carrier of R)

    proof

      let R,S be non empty RelStr, x be Element of (R [*] S);

      x in the carrier of (R [*] S);

      then x in (the carrier of S \/ the carrier of R) by Def2;

      then x in (the carrier of R \/ (the carrier of S \ the carrier of R)) by XBOOLE_1: 39;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: LATSUM_1:8



     Th8: for R,S be non empty RelStr holds for x,y be Element of R, a,b be Element of (R [*] S) st x = a & y = b & R tolerates S & R is transitive holds x <= y iff a <= b

    proof

      let R,S be non empty RelStr, x,y be Element of R, a,b be Element of (R [*] S);

      assume

       A1: x = a & y = b;

      assume

       A2: R tolerates S & R is transitive;

      hereby

        assume x <= y;

        then [x, y] in the InternalRel of R by ORDERS_2:def 5;

        then [a, b] in the InternalRel of (R [*] S) by A1, Th6;

        hence a <= b by ORDERS_2:def 5;

      end;

      assume a <= b;

      then [a, b] in the InternalRel of (R [*] S) by ORDERS_2:def 5;

      then [x, y] in the InternalRel of R by A1, A2, Th4;

      hence thesis by ORDERS_2:def 5;

    end;

    theorem :: LATSUM_1:9



     Th9: for R,S be non empty RelStr, a,b be Element of (R [*] S), c,d be Element of S st a = c & b = d & R tolerates S & S is transitive holds a <= b iff c <= d

    proof

      let R,S be non empty RelStr, a,b be Element of (R [*] S), c,d be Element of S;

      assume that

       A1: a = c & b = d and

       A2: R tolerates S & S is transitive;

      hereby

        assume a <= b;

        then [a, b] in the InternalRel of (R [*] S) by ORDERS_2:def 5;

        then [c, d] in the InternalRel of S by A1, A2, Th5;

        hence c <= d by ORDERS_2:def 5;

      end;

      assume c <= d;

      then [c, d] in the InternalRel of S by ORDERS_2:def 5;

      then [a, b] in the InternalRel of (R [*] S) by A1, Th6;

      hence thesis by ORDERS_2:def 5;

    end;

    theorem :: LATSUM_1:10



     Th10: for R,S be antisymmetric reflexive transitive with_suprema non empty RelStr holds for x be set st x in the carrier of R holds x is Element of (R [*] S)

    proof

      let R,S be antisymmetric reflexive transitive with_suprema non empty RelStr;

      let x be set;

      assume x in the carrier of R;

      then x in (the carrier of R \/ the carrier of S) by XBOOLE_0:def 3;

      hence thesis by Def2;

    end;

    theorem :: LATSUM_1:11

    for R,S be antisymmetric reflexive transitive with_suprema non empty RelStr holds for x be set st x in the carrier of S holds x is Element of (R [*] S)

    proof

      let R,S be antisymmetric reflexive transitive with_suprema non empty RelStr;

      let x be set;

      assume x in the carrier of S;

      then x in (the carrier of R \/ the carrier of S) by XBOOLE_0:def 3;

      hence thesis by Def2;

    end;

    theorem :: LATSUM_1:12



     Th12: for R,S be non empty RelStr holds for x be set st x in (the carrier of R /\ the carrier of S) holds x is Element of R

    proof

      let R,S be non empty RelStr;

      let x be set;

      assume

       A1: x in (the carrier of R /\ the carrier of S);

      (the carrier of R /\ the carrier of S) c= the carrier of R by XBOOLE_1: 17;

      hence thesis by A1;

    end;

    theorem :: LATSUM_1:13



     Th13: for R,S be non empty RelStr holds for x be set st x in (the carrier of R /\ the carrier of S) holds x is Element of S

    proof

      let R,S be non empty RelStr;

      let x be set;

      assume

       A1: x in (the carrier of R /\ the carrier of S);

      (the carrier of R /\ the carrier of S) c= the carrier of S by XBOOLE_1: 17;

      hence thesis by A1;

    end;

    theorem :: LATSUM_1:14

    for R,S be antisymmetric reflexive transitive with_suprema non empty RelStr holds for x,y be Element of (R [*] S) st x in the carrier of R & y in the carrier of S & R tolerates S holds x <= y iff (ex a be Element of (R [*] S) st a in (the carrier of R /\ the carrier of S) & x <= a & a <= y)

    proof

      let R,S be antisymmetric reflexive transitive with_suprema non empty RelStr, x,y be Element of (R [*] S);

      assume that

       A1: x in the carrier of R and

       A2: y in the carrier of S and

       A3: R tolerates S;

      per cases ;

        suppose

         A4: [x, y] in the InternalRel of R;

        hereby

          assume

           A5: x <= y;

          take a = y;

          y in the carrier of R by A4, ZFMISC_1: 87;

          hence a in (the carrier of R /\ the carrier of S) by A2, XBOOLE_0:def 4;

          (R [*] S) is reflexive by Th3;

          hence x <= a & a <= y by A5, ORDERS_2: 1;

        end;

         [x, y] in the InternalRel of (R [*] S) by A4, Th6;

        hence thesis by ORDERS_2:def 5;

      end;

        suppose

         A6: [x, y] in the InternalRel of S;

        hereby

          assume

           A7: x <= y;

          take a = x;

          x in the carrier of S by A6, ZFMISC_1: 87;

          hence a in (the carrier of R /\ the carrier of S) by A1, XBOOLE_0:def 4;

          (R [*] S) is reflexive by Th3;

          hence x <= a & a <= y by A7, ORDERS_2: 1;

        end;

         [x, y] in the InternalRel of (R [*] S) by A6, Th6;

        hence thesis by ORDERS_2:def 5;

      end;

        suppose that

         A8: ( not [x, y] in the InternalRel of R) & not [x, y] in the InternalRel of S;

        hereby

          assume x <= y;

          then [x, y] in the InternalRel of (R [*] S) by ORDERS_2:def 5;

          then [x, y] in ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by Def2;

          then [x, y] in (the InternalRel of R \/ the InternalRel of S) or [x, y] in (the InternalRel of R * the InternalRel of S) by XBOOLE_0:def 3;

          then

          consider z be object such that

           A9: [x, z] in the InternalRel of R and

           A10: [z, y] in the InternalRel of S by A8, RELAT_1:def 8, XBOOLE_0:def 3;



           A11: z in the carrier of R by A9, ZFMISC_1: 87;



           A12: z in the carrier of S by A10, ZFMISC_1: 87;

          then z in (the carrier of R \/ the carrier of S) by XBOOLE_0:def 3;

          then

          reconsider z as Element of (R [*] S) by Def2;

          take z;

          thus z in (the carrier of R /\ the carrier of S) by A11, A12, XBOOLE_0:def 4;

           [x, z] in the InternalRel of (R [*] S) by A9, Th6;

          hence x <= z by ORDERS_2:def 5;

           [z, y] in the InternalRel of (R [*] S) by A10, Th6;

          hence z <= y by ORDERS_2:def 5;

        end;

        given a be Element of (R [*] S) such that

         A13: a in (the carrier of R /\ the carrier of S) and

         A14: x <= a and

         A15: a <= y;

        reconsider y9 = y, a1 = a as Element of S by A2, A13, Th13;

        a1 <= y9 by A3, A15, Th9;

        then

         A16: [a, y] in the InternalRel of S by ORDERS_2:def 5;

        reconsider x9 = x, a9 = a as Element of R by A1, A13, Th12;

        x9 <= a9 by A3, A14, Th8;

        then [x, a] in the InternalRel of R by ORDERS_2:def 5;

        then [x, y] in (the InternalRel of R * the InternalRel of S) by A16, RELAT_1:def 8;

        then [x, y] in ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by XBOOLE_0:def 3;

        then [x, y] in the InternalRel of (R [*] S) by Def2;

        hence thesis by ORDERS_2:def 5;

      end;

    end;

    theorem :: LATSUM_1:15



     Th15: for R,S be non empty RelStr, a,b be Element of R, c,d be Element of S st a = c & b = d & R tolerates S & R is transitive & S is transitive holds a <= b iff c <= d

    proof

      let R,S be non empty RelStr, a,b be Element of R, c,d be Element of S;

      assume that

       A1: a = c & b = d and

       A2: R tolerates S and

       A3: R is transitive and

       A4: S is transitive;

      a in (the carrier of R \/ the carrier of S) & b in (the carrier of R \/ the carrier of S) by XBOOLE_0:def 3;

      then

      reconsider a9 = a, b9 = b as Element of (R [*] S) by Def2;

      hereby

        assume a <= b;

        then a9 <= b9 by A2, A3, Th8;

        hence c <= d by A1, A2, A4, Th9;

      end;

      assume c <= d;

      then a9 <= b9 by A1, A2, A4, Th9;

      hence thesis by A2, A3, Th8;

    end;

    theorem :: LATSUM_1:16



     Th16: for R be antisymmetric reflexive transitive with_suprema non empty RelStr, D be lower directed Subset of R holds for x,y be Element of R st x in D & y in D holds (x "\/" y) in D

    proof

      let R be antisymmetric reflexive transitive with_suprema non empty RelStr, D be lower directed Subset of R;

      let x,y be Element of R;

      assume x in D & y in D;

      then

      consider z be Element of R such that

       A1: z in D and

       A2: x <= z & y <= z by WAYBEL_0:def 1;

      (x "\/" y) <= z by A2, YELLOW_0: 22;

      hence thesis by A1, WAYBEL_0:def 19;

    end;

    theorem :: LATSUM_1:17



     Th17: for R,S be RelStr, a,b be set st (the carrier of R /\ the carrier of S) is upper Subset of R & [a, b] in the InternalRel of (R [*] S) & a in the carrier of S holds b in the carrier of S

    proof

      let R,S be RelStr, a,b be set;

      set X = (the carrier of R /\ the carrier of S);

      reconsider X as Subset of R by XBOOLE_1: 17;

      assume that

       A1: (the carrier of R /\ the carrier of S) is upper Subset of R and

       A2: [a, b] in the InternalRel of (R [*] S) and

       A3: a in the carrier of S;

       [a, b] in ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by A2, Def2;

      then

       A4: [a, b] in (the InternalRel of R \/ the InternalRel of S) or [a, b] in (the InternalRel of R * the InternalRel of S) by XBOOLE_0:def 3;

      assume

       A5: not b in the carrier of S;

      per cases by A4, XBOOLE_0:def 3;

        suppose

         A6: [a, b] in the InternalRel of R;

        then

        reconsider a9 = a, b9 = b as Element of R by ZFMISC_1: 87;

        a in the carrier of R by A6, ZFMISC_1: 87;

        then

         A7: a in (the carrier of R /\ the carrier of S) by A3, XBOOLE_0:def 4;

        a9 <= b9 by A6, ORDERS_2:def 5;

        then X c= the carrier of S & b in X by A1, A7, WAYBEL_0:def 20, XBOOLE_1: 17;

        hence thesis by A5;

      end;

        suppose [a, b] in the InternalRel of S;

        hence thesis by A5, ZFMISC_1: 87;

      end;

        suppose [a, b] in (the InternalRel of R * the InternalRel of S);

        hence thesis by A5, ZFMISC_1: 87;

      end;

    end;

    theorem :: LATSUM_1:18



     Th18: for R,S be RelStr, a,b be Element of (R [*] S) st (the carrier of R /\ the carrier of S) is upper Subset of R & a <= b & a in the carrier of S holds b in the carrier of S

    proof

      let R,S be RelStr, a,b be Element of (R [*] S);

      assume that

       A1: (the carrier of R /\ the carrier of S) is upper Subset of R and

       A2: a <= b and

       A3: a in the carrier of S;

       [a, b] in the InternalRel of (R [*] S) by A2, ORDERS_2:def 5;

      hence thesis by A1, A3, Th17;

    end;

    theorem :: LATSUM_1:19

    for R,S be antisymmetric reflexive transitive with_suprema non empty RelStr holds for x,y be Element of R, a,b be Element of S st (the carrier of R /\ the carrier of S) is lower directed Subset of S & (the carrier of R /\ the carrier of S) is upper Subset of R & R tolerates S & x = a & y = b holds (x "\/" y) = (a "\/" b)

    proof

      let R,S be antisymmetric reflexive transitive with_suprema non empty RelStr;

      let x,y be Element of R;

      let a,b be Element of S;

      assume that

       A1: (the carrier of R /\ the carrier of S) is lower directed Subset of S and

       A2: (the carrier of R /\ the carrier of S) is upper Subset of R and

       A3: R tolerates S and

       A4: x = a and

       A5: y = b;

      a in (the carrier of R /\ the carrier of S) & b in (the carrier of R /\ the carrier of S) by A4, A5, XBOOLE_0:def 4;

      then

      reconsider xy = (a "\/" b) as Element of R by A1, Th13, Th16;

      (a "\/" b) >= b by YELLOW_0: 22;

      then

       A6: xy >= y by A3, A5, Th15;



       A7: for d be Element of R st d >= x & d >= y holds xy <= d

      proof

        let d be Element of R;

        reconsider X = x, D = d as Element of (R [*] S) by Th10;

        assume that

         A8: d >= x and

         A9: d >= y;

        X <= D by A3, A8, Th8;

        then

        reconsider dd = d as Element of S by A2, A4, Th18;

        dd >= a & b <= dd by A3, A4, A5, A8, A9, Th15;

        then (a "\/" b) <= dd by YELLOW_5: 9;

        hence thesis by A3, Th15;

      end;

      (a "\/" b) >= a by YELLOW_0: 22;

      then xy >= x by A3, A4, Th15;

      hence thesis by A6, A7, YELLOW_0: 22;

    end;

    theorem :: LATSUM_1:20

    for R,S be lower-bounded antisymmetric reflexive transitive with_suprema non empty RelStr st (the carrier of R /\ the carrier of S) is non empty lower directed Subset of S holds ( Bottom S) in the carrier of R

    proof

      let R,S be lower-bounded antisymmetric reflexive transitive with_suprema non empty RelStr;

      assume

       A1: (the carrier of R /\ the carrier of S) is non empty lower directed Subset of S;

      then

      consider x be object such that

       A2: x in (the carrier of R /\ the carrier of S) by XBOOLE_0:def 1;

      reconsider x as Element of S by A2, Th13;

      ( Bottom S) <= x by YELLOW_0: 44;

      then ( Bottom S) in (the carrier of R /\ the carrier of S) by A1, A2, WAYBEL_0:def 19;

      hence thesis by XBOOLE_0:def 4;

    end;

    theorem :: LATSUM_1:21



     Th21: for R,S be RelStr, a,b be set st (the carrier of R /\ the carrier of S) is lower Subset of S & [a, b] in the InternalRel of (R [*] S) & b in the carrier of R holds a in the carrier of R

    proof

      let R,S be RelStr, a,b be set;

      set X = (the carrier of R /\ the carrier of S);

      reconsider X as Subset of R by XBOOLE_1: 17;

      assume that

       A1: (the carrier of R /\ the carrier of S) is lower Subset of S and

       A2: [a, b] in the InternalRel of (R [*] S) and

       A3: b in the carrier of R;

       [a, b] in ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by A2, Def2;

      then

       A4: [a, b] in (the InternalRel of R \/ the InternalRel of S) or [a, b] in (the InternalRel of R * the InternalRel of S) by XBOOLE_0:def 3;

      assume

       A5: not a in the carrier of R;

      per cases by A4, XBOOLE_0:def 3;

        suppose

         A6: [a, b] in the InternalRel of S;

        then

        reconsider a9 = a, b9 = b as Element of S by ZFMISC_1: 87;

        b in the carrier of S by A6, ZFMISC_1: 87;

        then

         A7: b in (the carrier of R /\ the carrier of S) by A3, XBOOLE_0:def 4;

        a9 <= b9 by A6, ORDERS_2:def 5;

        then a in X by A1, A7, WAYBEL_0:def 19;

        hence thesis by A5;

      end;

        suppose [a, b] in the InternalRel of R;

        hence thesis by A5, ZFMISC_1: 87;

      end;

        suppose [a, b] in (the InternalRel of R * the InternalRel of S);

        hence thesis by A5, ZFMISC_1: 87;

      end;

    end;

    theorem :: LATSUM_1:22

    for x,y be set, R,S be RelStr st [x, y] in the InternalRel of (R [*] S) & (the carrier of R /\ the carrier of S) is upper Subset of R holds x in the carrier of R & y in the carrier of R or x in the carrier of S & y in the carrier of S or x in (the carrier of R \ the carrier of S) & y in (the carrier of S \ the carrier of R)

    proof

      let x,y be set, R,S be RelStr;

      assume that

       A1: [x, y] in the InternalRel of (R [*] S) and

       A2: (the carrier of R /\ the carrier of S) is upper Subset of R;

      x in the carrier of (R [*] S) by A1, ZFMISC_1: 87;

      then

       A3: x in (the carrier of R \/ the carrier of S) by Def2;

      y in the carrier of (R [*] S) by A1, ZFMISC_1: 87;

      then

       A4: y in (the carrier of R \/ the carrier of S) by Def2;

      per cases by A3, A4, XBOOLE_0:def 3;

        suppose x in the carrier of R & y in the carrier of R;

        hence thesis;

      end;

        suppose x in the carrier of S & y in the carrier of S;

        hence thesis;

      end;

        suppose x in the carrier of R & y in the carrier of S;

        hence thesis by XBOOLE_0:def 5;

      end;

        suppose x in the carrier of S & y in the carrier of R;

        hence thesis by A1, A2, Th17;

      end;

    end;

    theorem :: LATSUM_1:23

    for R,S be RelStr, a,b be Element of (R [*] S) st (the carrier of R /\ the carrier of S) is lower Subset of S & a <= b & b in the carrier of R holds a in the carrier of R

    proof

      let R,S be RelStr, a,b be Element of (R [*] S);

      assume that

       A1: (the carrier of R /\ the carrier of S) is lower Subset of S and

       A2: a <= b and

       A3: b in the carrier of R;

       [a, b] in the InternalRel of (R [*] S) by A2, ORDERS_2:def 5;

      hence thesis by A1, A3, Th21;

    end;

    theorem :: LATSUM_1:24

    for R,S be RelStr st R tolerates S & (the carrier of R /\ the carrier of S) is upper Subset of R & (the carrier of R /\ the carrier of S) is lower Subset of S & R is transitive antisymmetric & S is transitive antisymmetric holds (R [*] S) is antisymmetric

    proof

      let R,S be RelStr;

      set X = the carrier of (R [*] S), F = the InternalRel of (R [*] S);

      assume that

       A1: R tolerates S and

       A2: (the carrier of R /\ the carrier of S) is upper Subset of R and

       A3: (the carrier of R /\ the carrier of S) is lower Subset of S and

       A4: R is transitive antisymmetric and

       A5: S is transitive antisymmetric;



       A6: the InternalRel of S is_antisymmetric_in the carrier of S by A5, ORDERS_2:def 4;



       A7: the InternalRel of R is_antisymmetric_in the carrier of R by A4, ORDERS_2:def 4;

      F is_antisymmetric_in X

      proof

        let x,y be object;

        assume that

         A8: x in X & y in X and

         A9: [x, y] in F and

         A10: [y, x] in F;



         A11: x in (the carrier of R \/ the carrier of S) & y in (the carrier of R \/ the carrier of S) by A8, Def2;

        per cases by A11, XBOOLE_0:def 3;

          suppose

           A12: x in the carrier of R & y in the carrier of R;

          then [x, y] in the InternalRel of R & [y, x] in the InternalRel of R by A1, A4, A9, A10, Th4;

          hence thesis by A7, A12;

        end;

          suppose

           A13: x in the carrier of R & y in the carrier of S;

          then

           A14: y in the carrier of R by A3, A10, Th21;

          then [x, y] in the InternalRel of R & [y, x] in the InternalRel of R by A1, A4, A9, A10, A13, Th4;

          hence thesis by A7, A13, A14;

        end;

          suppose

           A15: x in the carrier of S & y in the carrier of R;

          then

           A16: y in the carrier of S by A2, A9, Th17;

          then [x, y] in the InternalRel of S & [y, x] in the InternalRel of S by A1, A5, A9, A10, A15, Th5;

          hence thesis by A6, A15, A16;

        end;

          suppose

           A17: x in the carrier of S & y in the carrier of S;

          then [x, y] in the InternalRel of S & [y, x] in the InternalRel of S by A1, A5, A9, A10, Th5;

          hence thesis by A6, A17;

        end;

      end;

      hence thesis by ORDERS_2:def 4;

    end;

    theorem :: LATSUM_1:25

    for R,S be RelStr st (the carrier of R /\ the carrier of S) is upper Subset of R & (the carrier of R /\ the carrier of S) is lower Subset of S & R tolerates S & R is transitive & S is transitive holds (R [*] S) is transitive

    proof

      let R,S be RelStr;

      set X = the carrier of (R [*] S), F = the InternalRel of (R [*] S);

      assume that

       A1: (the carrier of R /\ the carrier of S) is upper Subset of R and

       A2: (the carrier of R /\ the carrier of S) is lower Subset of S and

       A3: R tolerates S and

       A4: R is transitive and

       A5: S is transitive;



       A6: the InternalRel of S is_transitive_in the carrier of S by A5, ORDERS_2:def 3;



       A7: the InternalRel of R is_transitive_in the carrier of R by A4, ORDERS_2:def 3;

      F is_transitive_in X

      proof

        let x,y,z be object;

        assume that

         A8: x in X & y in X and

         A9: z in X and

         A10: [x, y] in F and

         A11: [y, z] in F;



         A12: x in (the carrier of R \/ the carrier of S) & y in (the carrier of R \/ the carrier of S) by A8, Def2;



         A13: z in (the carrier of R \/ the carrier of S) by A9, Def2;

        per cases by A12, A13, XBOOLE_0:def 3;

          suppose

           A14: x in the carrier of R & y in the carrier of R & z in the carrier of R;

          then [x, y] in the InternalRel of R & [y, z] in the InternalRel of R by A3, A4, A10, A11, Th4;

          then [x, z] in the InternalRel of R by A7, A14;

          hence thesis by Th6;

        end;

          suppose

           A15: x in the carrier of R & y in the carrier of R & z in the carrier of S;

          then

           A16: [x, y] in the InternalRel of R by A3, A4, A10, Th4;

           [y, z] in ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by A11, Def2;

          then

           A17: [y, z] in (the InternalRel of R \/ the InternalRel of S) or [y, z] in (the InternalRel of R * the InternalRel of S) by XBOOLE_0:def 3;

          now

            per cases by A17, XBOOLE_0:def 3;

              suppose

               A18: [y, z] in the InternalRel of R;

              then z in the carrier of R by ZFMISC_1: 87;

              then [x, z] in the InternalRel of R by A7, A15, A16, A18;

              hence thesis by Th6;

            end;

              suppose [y, z] in the InternalRel of S;

              then [x, z] in (the InternalRel of R * the InternalRel of S) by A16, RELAT_1:def 8;

              then [x, z] in ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by XBOOLE_0:def 3;

              hence thesis by Def2;

            end;

              suppose [y, z] in (the InternalRel of R * the InternalRel of S);

              then

              consider a be object such that

               A19: [y, a] in the InternalRel of R and

               A20: [a, z] in the InternalRel of S by RELAT_1:def 8;

              a in the carrier of R by A19, ZFMISC_1: 87;

              then [x, a] in the InternalRel of R by A7, A15, A16, A19;

              then [x, z] in (the InternalRel of R * the InternalRel of S) by A20, RELAT_1:def 8;

              then [x, z] in ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by XBOOLE_0:def 3;

              hence thesis by Def2;

            end;

          end;

          hence thesis;

        end;

          suppose

           A21: x in the carrier of R & y in the carrier of S & z in the carrier of R;

          then

           A22: y in the carrier of R by A2, A11, Th21;

          then [x, y] in the InternalRel of R & [y, z] in the InternalRel of R by A3, A4, A10, A11, A21, Th4;

          then [x, z] in the InternalRel of R by A7, A21, A22;

          hence thesis by Th6;

        end;

          suppose

           A23: x in the carrier of S & y in the carrier of R & z in the carrier of R;

          then

           A24: [y, z] in the InternalRel of R by A3, A4, A11, Th4;



           A25: x in the carrier of R by A2, A10, A23, Th21;

          then [x, y] in the InternalRel of R by A3, A4, A10, A23, Th4;

          then [x, z] in the InternalRel of R by A7, A23, A25, A24;

          hence thesis by Th6;

        end;

          suppose

           A26: x in the carrier of S & y in the carrier of S & z in the carrier of R;

          then

           A27: [x, y] in the InternalRel of S by A3, A5, A10, Th5;



           A28: z in the carrier of S by A1, A11, A26, Th17;

          then [y, z] in the InternalRel of S by A3, A5, A11, A26, Th5;

          then [x, z] in the InternalRel of S by A6, A26, A27, A28;

          hence thesis by Th6;

        end;

          suppose

           A29: x in the carrier of S & y in the carrier of S & z in the carrier of S;

          then [x, y] in the InternalRel of S & [y, z] in the InternalRel of S by A3, A5, A10, A11, Th5;

          then [x, z] in the InternalRel of S by A6, A29;

          hence thesis by Th6;

        end;

          suppose

           A30: x in the carrier of R & y in the carrier of S & z in the carrier of S;

          then

           A31: [y, z] in the InternalRel of S by A3, A5, A11, Th5;

           [x, y] in ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by A10, Def2;

          then

           A32: [x, y] in (the InternalRel of R \/ the InternalRel of S) or [x, y] in (the InternalRel of R * the InternalRel of S) by XBOOLE_0:def 3;

          now

            per cases by A32, XBOOLE_0:def 3;

              suppose [x, y] in the InternalRel of R;

              then [x, z] in (the InternalRel of R * the InternalRel of S) by A31, RELAT_1:def 8;

              then [x, z] in ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by XBOOLE_0:def 3;

              hence thesis by Def2;

            end;

              suppose

               A33: [x, y] in the InternalRel of S;

              then x in the carrier of S by ZFMISC_1: 87;

              then [x, z] in the InternalRel of S by A6, A30, A31, A33;

              hence thesis by Th6;

            end;

              suppose [x, y] in (the InternalRel of R * the InternalRel of S);

              then

              consider a be object such that

               A34: [x, a] in the InternalRel of R and

               A35: [a, y] in the InternalRel of S by RELAT_1:def 8;

              a in the carrier of S by A35, ZFMISC_1: 87;

              then [a, z] in the InternalRel of S by A6, A30, A31, A35;

              then [x, z] in (the InternalRel of R * the InternalRel of S) by A34, RELAT_1:def 8;

              then [x, z] in ((the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S)) by XBOOLE_0:def 3;

              hence thesis by Def2;

            end;

          end;

          hence thesis;

        end;

          suppose

           A36: x in the carrier of S & y in the carrier of R & z in the carrier of S;

          then

           A37: y in the carrier of S by A1, A10, Th17;

          then [x, y] in the InternalRel of S & [y, z] in the InternalRel of S by A3, A5, A10, A11, A36, Th5;

          then [x, z] in the InternalRel of S by A6, A36, A37;

          hence thesis by Th6;

        end;

      end;

      hence thesis by ORDERS_2:def 3;

    end;