:: by Artur Korni{\l}owicz

::

:: Received September 25, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

theorem Th1: :: YELLOW_4:1

for L being RelStr

for X being set

for a being Element of L st a in X & ex_sup_of X,L holds

a <= "\/" (X,L)

for X being set

for a being Element of L st a in X & ex_sup_of X,L holds

a <= "\/" (X,L)

proof end;

theorem Th2: :: YELLOW_4:2

for L being RelStr

for X being set

for a being Element of L st a in X & ex_inf_of X,L holds

"/\" (X,L) <= a

for X being set

for a being Element of L st a in X & ex_inf_of X,L holds

"/\" (X,L) <= a

proof end;

definition

let L be RelStr ;

let A, B be Subset of L;

end;
let A, B be Subset of L;

pred A is_finer_than B means :Def1: :: YELLOW_4:def 1

for a being Element of L st a in A holds

ex b being Element of L st

( b in B & a <= b );

for a being Element of L st a in A holds

ex b being Element of L st

( b in B & a <= b );

pred B is_coarser_than A means :Def2: :: YELLOW_4:def 2

for b being Element of L st b in B holds

ex a being Element of L st

( a in A & a <= b );

for b being Element of L st b in B holds

ex a being Element of L st

( a in A & a <= b );

:: deftheorem Def1 defines is_finer_than YELLOW_4:def 1 :

for L being RelStr

for A, B being Subset of L holds

( A is_finer_than B iff for a being Element of L st a in A holds

ex b being Element of L st

( b in B & a <= b ) );

for L being RelStr

for A, B being Subset of L holds

( A is_finer_than B iff for a being Element of L st a in A holds

ex b being Element of L st

( b in B & a <= b ) );

:: deftheorem Def2 defines is_coarser_than YELLOW_4:def 2 :

for L being RelStr

for A, B being Subset of L holds

( B is_coarser_than A iff for b being Element of L st b in B holds

ex a being Element of L st

( a in A & a <= b ) );

for L being RelStr

for A, B being Subset of L holds

( B is_coarser_than A iff for b being Element of L st b in B holds

ex a being Element of L st

( a in A & a <= b ) );

definition

let L be non empty reflexive RelStr ;

let A, B be Subset of L;

:: original: is_finer_than

redefine pred A is_finer_than B;

reflexivity

for A being Subset of L holds (L,b_{1},b_{1})

redefine pred B is_coarser_than A;

reflexivity

for B being Subset of L holds (L,b_{1},b_{1})

end;
let A, B be Subset of L;

:: original: is_finer_than

redefine pred A is_finer_than B;

reflexivity

for A being Subset of L holds (L,b

proof end;

:: original: is_coarser_thanredefine pred B is_coarser_than A;

reflexivity

for B being Subset of L holds (L,b

proof end;

theorem :: YELLOW_4:4

for L being transitive RelStr

for A, B, C being Subset of L st A is_finer_than B & B is_finer_than C holds

A is_finer_than C

for A, B, C being Subset of L st A is_finer_than B & B is_finer_than C holds

A is_finer_than C

proof end;

theorem :: YELLOW_4:7

for L being transitive RelStr

for A, B, C being Subset of L st C is_coarser_than B & B is_coarser_than A holds

C is_coarser_than A

for A, B, C being Subset of L st C is_coarser_than B & B is_coarser_than A holds

C is_coarser_than A

proof end;

begin

definition

let L be non empty RelStr ;

let D1, D2 be Subset of L;

{ (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 ) } is Subset of L

end;
let D1, D2 be Subset of L;

func D1 "\/" D2 -> Subset of L equals :: YELLOW_4:def 3

{ (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ;

coherence { (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ;

{ (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 ) } is Subset of L

proof end;

:: deftheorem defines "\/" YELLOW_4:def 3 :

for L being non empty RelStr

for D1, D2 being Subset of L holds D1 "\/" D2 = { (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ;

for L being non empty RelStr

for D1, D2 being Subset of L holds D1 "\/" D2 = { (x "\/" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ;

definition

let L be antisymmetric with_suprema RelStr ;

let D1, D2 be Subset of L;

:: original: "\/"

redefine func D1 "\/" D2 -> Subset of L;

commutativity

for D1, D2 being Subset of L holds D1 "\/" D2 = D2 "\/" D1

end;
let D1, D2 be Subset of L;

:: original: "\/"

redefine func D1 "\/" D2 -> Subset of L;

commutativity

for D1, D2 being Subset of L holds D1 "\/" D2 = D2 "\/" D1

proof end;

theorem :: YELLOW_4:10

theorem :: YELLOW_4:11

for L being antisymmetric with_suprema RelStr

for A being Subset of L

for B being non empty Subset of L holds A is_finer_than A "\/" B

for A being Subset of L

for B being non empty Subset of L holds A is_finer_than A "\/" B

proof end;

theorem :: YELLOW_4:12

for L being antisymmetric with_suprema RelStr

for A, B being Subset of L holds A "\/" B is_coarser_than A

for A, B being Subset of L holds A "\/" B is_coarser_than A

proof end;

theorem :: YELLOW_4:14

for L being transitive antisymmetric with_suprema RelStr

for D1, D2, D3 being Subset of L holds (D1 "\/" D2) "\/" D3 = D1 "\/" (D2 "\/" D3)

for D1, D2, D3 being Subset of L holds (D1 "\/" D2) "\/" D3 = D1 "\/" (D2 "\/" D3)

proof end;

registration

let L be non empty RelStr ;

let D1, D2 be non empty Subset of L;

coherence

not D1 "\/" D2 is empty

end;
let D1, D2 be non empty Subset of L;

coherence

not D1 "\/" D2 is empty

proof end;

registration

let L be transitive antisymmetric with_suprema RelStr ;

let D1, D2 be directed Subset of L;

coherence

D1 "\/" D2 is directed

end;
let D1, D2 be directed Subset of L;

coherence

D1 "\/" D2 is directed

proof end;

registration

let L be transitive antisymmetric with_suprema RelStr ;

let D1, D2 be filtered Subset of L;

coherence

D1 "\/" D2 is filtered

end;
let D1, D2 be filtered Subset of L;

coherence

D1 "\/" D2 is filtered

proof end;

registration

let L be with_suprema Poset;

let D1, D2 be upper Subset of L;

coherence

D1 "\/" D2 is upper

end;
let D1, D2 be upper Subset of L;

coherence

D1 "\/" D2 is upper

proof end;

theorem Th15: :: YELLOW_4:15

for L being non empty RelStr

for Y being Subset of L

for x being Element of L holds {x} "\/" Y = { (x "\/" y) where y is Element of L : y in Y }

for Y being Subset of L

for x being Element of L holds {x} "\/" Y = { (x "\/" y) where y is Element of L : y in Y }

proof end;

theorem :: YELLOW_4:16

for L being non empty RelStr

for A, B, C being Subset of L holds A "\/" (B \/ C) = (A "\/" B) \/ (A "\/" C)

for A, B, C being Subset of L holds A "\/" (B \/ C) = (A "\/" B) \/ (A "\/" C)

proof end;

theorem :: YELLOW_4:17

for L being reflexive antisymmetric with_suprema RelStr

for A, B, C being Subset of L holds A \/ (B "\/" C) c= (A \/ B) "\/" (A \/ C)

for A, B, C being Subset of L holds A \/ (B "\/" C) c= (A \/ B) "\/" (A \/ C)

proof end;

theorem :: YELLOW_4:18

for L being antisymmetric with_suprema RelStr

for A being upper Subset of L

for B, C being Subset of L holds (A \/ B) "\/" (A \/ C) c= A \/ (B "\/" C)

for A being upper Subset of L

for B, C being Subset of L holds (A \/ B) "\/" (A \/ C) c= A \/ (B "\/" C)

proof end;

Lm1: now :: thesis: for L being non empty RelStr

for x, y being Element of L holds { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "\/" y)}

for x, y being Element of L holds { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "\/" y)}

let L be non empty RelStr ; :: thesis: for x, y being Element of L holds { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "\/" y)}

let x, y be Element of L; :: thesis: { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "\/" y)}

thus { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "\/" y)} :: thesis: verum

end;
let x, y be Element of L; :: thesis: { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "\/" y)}

thus { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "\/" y)} :: thesis: verum

proof

thus
{ (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } c= {(x "\/" y)}
:: according to XBOOLE_0:def 10 :: thesis: {(x "\/" y)} c= { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) }

assume q in {(x "\/" y)} ; :: thesis: q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) }

then A3: q = x "\/" y by TARSKI:def 1;

( x in {x} & y in {y} ) by TARSKI:def 1;

hence q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } by A3; :: thesis: verum

end;
proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in {(x "\/" y)} or q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } )
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } or q in {(x "\/" y)} )

assume q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } ; :: thesis: q in {(x "\/" y)}

then consider u, v being Element of L such that

A1: q = u "\/" v and

A2: ( u in {x} & v in {y} ) ;

( u = x & v = y ) by A2, TARSKI:def 1;

hence q in {(x "\/" y)} by A1, TARSKI:def 1; :: thesis: verum

end;
assume q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } ; :: thesis: q in {(x "\/" y)}

then consider u, v being Element of L such that

A1: q = u "\/" v and

A2: ( u in {x} & v in {y} ) ;

( u = x & v = y ) by A2, TARSKI:def 1;

hence q in {(x "\/" y)} by A1, TARSKI:def 1; :: thesis: verum

assume q in {(x "\/" y)} ; :: thesis: q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) }

then A3: q = x "\/" y by TARSKI:def 1;

( x in {x} & y in {y} ) by TARSKI:def 1;

hence q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y} ) } by A3; :: thesis: verum

Lm2: now :: thesis: for L being non empty RelStr

for x, y, z being Element of L holds { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)}

for x, y, z being Element of L holds { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)}

let L be non empty RelStr ; :: thesis: for x, y, z being Element of L holds { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)}

let x, y, z be Element of L; :: thesis: { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)}

thus { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)} :: thesis: verum

end;
let x, y, z be Element of L; :: thesis: { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)}

thus { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "\/" y),(x "\/" z)} :: thesis: verum

proof

thus
{ (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } c= {(x "\/" y),(x "\/" z)}
:: according to XBOOLE_0:def 10 :: thesis: {(x "\/" y),(x "\/" z)} c= { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }

A5: z in {y,z} by TARSKI:def 2;

assume q in {(x "\/" y),(x "\/" z)} ; :: thesis: q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }

then A6: ( q = x "\/" y or q = x "\/" z ) by TARSKI:def 2;

( x in {x} & y in {y,z} ) by TARSKI:def 1, TARSKI:def 2;

hence q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } by A6, A5; :: thesis: verum

end;
proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in {(x "\/" y),(x "\/" z)} or q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } )
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } or q in {(x "\/" y),(x "\/" z)} )

assume q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } ; :: thesis: q in {(x "\/" y),(x "\/" z)}

then consider u, v being Element of L such that

A1: q = u "\/" v and

A2: u in {x} and

A3: v in {y,z} ;

A4: ( v = y or v = z ) by A3, TARSKI:def 2;

u = x by A2, TARSKI:def 1;

hence q in {(x "\/" y),(x "\/" z)} by A1, A4, TARSKI:def 2; :: thesis: verum

end;
assume q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } ; :: thesis: q in {(x "\/" y),(x "\/" z)}

then consider u, v being Element of L such that

A1: q = u "\/" v and

A2: u in {x} and

A3: v in {y,z} ;

A4: ( v = y or v = z ) by A3, TARSKI:def 2;

u = x by A2, TARSKI:def 1;

hence q in {(x "\/" y),(x "\/" z)} by A1, A4, TARSKI:def 2; :: thesis: verum

A5: z in {y,z} by TARSKI:def 2;

assume q in {(x "\/" y),(x "\/" z)} ; :: thesis: q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }

then A6: ( q = x "\/" y or q = x "\/" z ) by TARSKI:def 2;

( x in {x} & y in {y,z} ) by TARSKI:def 1, TARSKI:def 2;

hence q in { (a "\/" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } by A6, A5; :: thesis: verum

theorem :: YELLOW_4:19

theorem :: YELLOW_4:20

theorem :: YELLOW_4:21

for L being non empty RelStr

for X1, X2, Y1, Y2 being Subset of L st X1 c= Y1 & X2 c= Y2 holds

X1 "\/" X2 c= Y1 "\/" Y2

for X1, X2, Y1, Y2 being Subset of L st X1 c= Y1 & X2 c= Y2 holds

X1 "\/" X2 c= Y1 "\/" Y2

proof end;

theorem :: YELLOW_4:22

for L being reflexive antisymmetric with_suprema RelStr

for D being Subset of L

for x being Element of L st x is_<=_than D holds

{x} "\/" D = D

for D being Subset of L

for x being Element of L st x is_<=_than D holds

{x} "\/" D = D

proof end;

theorem :: YELLOW_4:23

for L being antisymmetric with_suprema RelStr

for D being Subset of L

for x being Element of L holds x is_<=_than {x} "\/" D

for D being Subset of L

for x being Element of L holds x is_<=_than {x} "\/" D

proof end;

theorem :: YELLOW_4:24

for L being with_suprema Poset

for X being Subset of L

for x being Element of L st ex_inf_of {x} "\/" X,L & ex_inf_of X,L holds

x "\/" (inf X) <= inf ({x} "\/" X)

for X being Subset of L

for x being Element of L st ex_inf_of {x} "\/" X,L & ex_inf_of X,L holds

x "\/" (inf X) <= inf ({x} "\/" X)

proof end;

theorem Th25: :: YELLOW_4:25

for L being non empty transitive antisymmetric complete RelStr

for A being Subset of L

for B being non empty Subset of L holds A is_<=_than sup (A "\/" B)

for A being Subset of L

for B being non empty Subset of L holds A is_<=_than sup (A "\/" B)

proof end;

theorem :: YELLOW_4:26

for L being transitive antisymmetric with_suprema RelStr

for a, b being Element of L

for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds

a "\/" b is_<=_than A "\/" B

for a, b being Element of L

for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds

a "\/" b is_<=_than A "\/" B

proof end;

theorem Th27: :: YELLOW_4:27

for L being transitive antisymmetric with_suprema RelStr

for a, b being Element of L

for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds

a "\/" b is_>=_than A "\/" B

for a, b being Element of L

for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds

a "\/" b is_>=_than A "\/" B

proof end;

theorem :: YELLOW_4:28

for L being non empty complete Poset

for A, B being non empty Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B)

for A, B being non empty Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B)

proof end;

theorem Th29: :: YELLOW_4:29

for L being antisymmetric with_suprema RelStr

for X being Subset of L

for Y being non empty Subset of L holds X c= downarrow (X "\/" Y)

for X being Subset of L

for Y being non empty Subset of L holds X c= downarrow (X "\/" Y)

proof end;

theorem :: YELLOW_4:30

for L being with_suprema Poset

for x, y being Element of (InclPoset (Ids L))

for X, Y being Subset of L st x = X & y = Y holds

x "\/" y = downarrow (X "\/" Y)

for x, y being Element of (InclPoset (Ids L))

for X, Y being Subset of L st x = X & y = Y holds

x "\/" y = downarrow (X "\/" Y)

proof end;

theorem :: YELLOW_4:31

for L being non empty RelStr

for D being Subset of [:L,L:] holds union { X where X is Subset of L : ex x being Element of L st

( X = {x} "\/" (proj2 D) & x in proj1 D ) } = (proj1 D) "\/" (proj2 D)

for D being Subset of [:L,L:] holds union { X where X is Subset of L : ex x being Element of L st

( X = {x} "\/" (proj2 D) & x in proj1 D ) } = (proj1 D) "\/" (proj2 D)

proof end;

theorem Th32: :: YELLOW_4:32

for L being transitive antisymmetric with_suprema RelStr

for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2)

for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2)

proof end;

theorem :: YELLOW_4:33

for L being with_suprema Poset

for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) = downarrow (D1 "\/" D2)

for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) = downarrow (D1 "\/" D2)

proof end;

theorem Th34: :: YELLOW_4:34

for L being transitive antisymmetric with_suprema RelStr

for D1, D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow (D1 "\/" D2)

for D1, D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow (D1 "\/" D2)

proof end;

theorem :: YELLOW_4:35

for L being with_suprema Poset

for D1, D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) = uparrow (D1 "\/" D2)

for D1, D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) = uparrow (D1 "\/" D2)

proof end;

begin

definition

let L be non empty RelStr ;

let D1, D2 be Subset of L;

{ (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } is Subset of L

end;
let D1, D2 be Subset of L;

func D1 "/\" D2 -> Subset of L equals :: YELLOW_4:def 4

{ (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ;

coherence { (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ;

{ (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } is Subset of L

proof end;

:: deftheorem defines "/\" YELLOW_4:def 4 :

for L being non empty RelStr

for D1, D2 being Subset of L holds D1 "/\" D2 = { (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ;

for L being non empty RelStr

for D1, D2 being Subset of L holds D1 "/\" D2 = { (x "/\" y) where x, y is Element of L : ( x in D1 & y in D2 ) } ;

definition

let L be antisymmetric with_infima RelStr ;

let D1, D2 be Subset of L;

:: original: "/\"

redefine func D1 "/\" D2 -> Subset of L;

commutativity

for D1, D2 being Subset of L holds D1 "/\" D2 = D2 "/\" D1

end;
let D1, D2 be Subset of L;

:: original: "/\"

redefine func D1 "/\" D2 -> Subset of L;

commutativity

for D1, D2 being Subset of L holds D1 "/\" D2 = D2 "/\" D1

proof end;

theorem :: YELLOW_4:37

theorem :: YELLOW_4:38

for L being antisymmetric with_infima RelStr

for A being Subset of L

for B being non empty Subset of L holds A is_coarser_than A "/\" B

for A being Subset of L

for B being non empty Subset of L holds A is_coarser_than A "/\" B

proof end;

theorem :: YELLOW_4:39

for L being antisymmetric with_infima RelStr

for A, B being Subset of L holds A "/\" B is_finer_than A

for A, B being Subset of L holds A "/\" B is_finer_than A

proof end;

theorem :: YELLOW_4:41

for L being transitive antisymmetric with_infima RelStr

for D1, D2, D3 being Subset of L holds (D1 "/\" D2) "/\" D3 = D1 "/\" (D2 "/\" D3)

for D1, D2, D3 being Subset of L holds (D1 "/\" D2) "/\" D3 = D1 "/\" (D2 "/\" D3)

proof end;

registration

let L be non empty RelStr ;

let D1, D2 be non empty Subset of L;

coherence

not D1 "/\" D2 is empty

end;
let D1, D2 be non empty Subset of L;

coherence

not D1 "/\" D2 is empty

proof end;

registration

let L be transitive antisymmetric with_infima RelStr ;

let D1, D2 be directed Subset of L;

coherence

D1 "/\" D2 is directed

end;
let D1, D2 be directed Subset of L;

coherence

D1 "/\" D2 is directed

proof end;

registration

let L be transitive antisymmetric with_infima RelStr ;

let D1, D2 be filtered Subset of L;

coherence

D1 "/\" D2 is filtered

end;
let D1, D2 be filtered Subset of L;

coherence

D1 "/\" D2 is filtered

proof end;

registration
end;

theorem Th42: :: YELLOW_4:42

for L being non empty RelStr

for Y being Subset of L

for x being Element of L holds {x} "/\" Y = { (x "/\" y) where y is Element of L : y in Y }

for Y being Subset of L

for x being Element of L holds {x} "/\" Y = { (x "/\" y) where y is Element of L : y in Y }

proof end;

theorem :: YELLOW_4:43

for L being non empty RelStr

for A, B, C being Subset of L holds A "/\" (B \/ C) = (A "/\" B) \/ (A "/\" C)

for A, B, C being Subset of L holds A "/\" (B \/ C) = (A "/\" B) \/ (A "/\" C)

proof end;

theorem :: YELLOW_4:44

for L being reflexive antisymmetric with_infima RelStr

for A, B, C being Subset of L holds A \/ (B "/\" C) c= (A \/ B) "/\" (A \/ C)

for A, B, C being Subset of L holds A \/ (B "/\" C) c= (A \/ B) "/\" (A \/ C)

proof end;

theorem :: YELLOW_4:45

for L being antisymmetric with_infima RelStr

for A being lower Subset of L

for B, C being Subset of L holds (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C)

for A being lower Subset of L

for B, C being Subset of L holds (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C)

proof end;

Lm3: now :: thesis: for L being non empty RelStr

for x, y being Element of L holds { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "/\" y)}

for x, y being Element of L holds { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "/\" y)}

let L be non empty RelStr ; :: thesis: for x, y being Element of L holds { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "/\" y)}

let x, y be Element of L; :: thesis: { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "/\" y)}

thus { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "/\" y)} :: thesis: verum

end;
let x, y be Element of L; :: thesis: { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "/\" y)}

thus { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } = {(x "/\" y)} :: thesis: verum

proof

thus
{ (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } c= {(x "/\" y)}
:: according to XBOOLE_0:def 10 :: thesis: {(x "/\" y)} c= { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) }

assume q in {(x "/\" y)} ; :: thesis: q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) }

then A3: q = x "/\" y by TARSKI:def 1;

( x in {x} & y in {y} ) by TARSKI:def 1;

hence q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } by A3; :: thesis: verum

end;
proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in {(x "/\" y)} or q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } )
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } or q in {(x "/\" y)} )

assume q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } ; :: thesis: q in {(x "/\" y)}

then consider u, v being Element of L such that

A1: q = u "/\" v and

A2: ( u in {x} & v in {y} ) ;

( u = x & v = y ) by A2, TARSKI:def 1;

hence q in {(x "/\" y)} by A1, TARSKI:def 1; :: thesis: verum

end;
assume q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } ; :: thesis: q in {(x "/\" y)}

then consider u, v being Element of L such that

A1: q = u "/\" v and

A2: ( u in {x} & v in {y} ) ;

( u = x & v = y ) by A2, TARSKI:def 1;

hence q in {(x "/\" y)} by A1, TARSKI:def 1; :: thesis: verum

assume q in {(x "/\" y)} ; :: thesis: q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) }

then A3: q = x "/\" y by TARSKI:def 1;

( x in {x} & y in {y} ) by TARSKI:def 1;

hence q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y} ) } by A3; :: thesis: verum

Lm4: now :: thesis: for L being non empty RelStr

for x, y, z being Element of L holds { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)}

for x, y, z being Element of L holds { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)}

let L be non empty RelStr ; :: thesis: for x, y, z being Element of L holds { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)}

let x, y, z be Element of L; :: thesis: { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)}

thus { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)} :: thesis: verum

end;
let x, y, z be Element of L; :: thesis: { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)}

thus { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } = {(x "/\" y),(x "/\" z)} :: thesis: verum

proof

thus
{ (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } c= {(x "/\" y),(x "/\" z)}
:: according to XBOOLE_0:def 10 :: thesis: {(x "/\" y),(x "/\" z)} c= { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }

A5: z in {y,z} by TARSKI:def 2;

assume q in {(x "/\" y),(x "/\" z)} ; :: thesis: q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }

then A6: ( q = x "/\" y or q = x "/\" z ) by TARSKI:def 2;

( x in {x} & y in {y,z} ) by TARSKI:def 1, TARSKI:def 2;

hence q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } by A6, A5; :: thesis: verum

end;
proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in {(x "/\" y),(x "/\" z)} or q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } )
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } or q in {(x "/\" y),(x "/\" z)} )

assume q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } ; :: thesis: q in {(x "/\" y),(x "/\" z)}

then consider u, v being Element of L such that

A1: q = u "/\" v and

A2: u in {x} and

A3: v in {y,z} ;

A4: ( v = y or v = z ) by A3, TARSKI:def 2;

u = x by A2, TARSKI:def 1;

hence q in {(x "/\" y),(x "/\" z)} by A1, A4, TARSKI:def 2; :: thesis: verum

end;
assume q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } ; :: thesis: q in {(x "/\" y),(x "/\" z)}

then consider u, v being Element of L such that

A1: q = u "/\" v and

A2: u in {x} and

A3: v in {y,z} ;

A4: ( v = y or v = z ) by A3, TARSKI:def 2;

u = x by A2, TARSKI:def 1;

hence q in {(x "/\" y),(x "/\" z)} by A1, A4, TARSKI:def 2; :: thesis: verum

A5: z in {y,z} by TARSKI:def 2;

assume q in {(x "/\" y),(x "/\" z)} ; :: thesis: q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) }

then A6: ( q = x "/\" y or q = x "/\" z ) by TARSKI:def 2;

( x in {x} & y in {y,z} ) by TARSKI:def 1, TARSKI:def 2;

hence q in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in {y,z} ) } by A6, A5; :: thesis: verum

theorem :: YELLOW_4:46

theorem :: YELLOW_4:47

theorem :: YELLOW_4:48

for L being non empty RelStr

for X1, X2, Y1, Y2 being Subset of L st X1 c= Y1 & X2 c= Y2 holds

X1 "/\" X2 c= Y1 "/\" Y2

for X1, X2, Y1, Y2 being Subset of L st X1 c= Y1 & X2 c= Y2 holds

X1 "/\" X2 c= Y1 "/\" Y2

proof end;

theorem Th49: :: YELLOW_4:49

for L being reflexive antisymmetric with_infima RelStr

for A, B being Subset of L holds A /\ B c= A "/\" B

for A, B being Subset of L holds A /\ B c= A "/\" B

proof end;

theorem Th50: :: YELLOW_4:50

for L being reflexive antisymmetric with_infima RelStr

for A, B being lower Subset of L holds A "/\" B = A /\ B

for A, B being lower Subset of L holds A "/\" B = A /\ B

proof end;

theorem :: YELLOW_4:51

for L being reflexive antisymmetric with_infima RelStr

for D being Subset of L

for x being Element of L st x is_>=_than D holds

{x} "/\" D = D

for D being Subset of L

for x being Element of L st x is_>=_than D holds

{x} "/\" D = D

proof end;

theorem :: YELLOW_4:52

for L being antisymmetric with_infima RelStr

for D being Subset of L

for x being Element of L holds {x} "/\" D is_<=_than x

for D being Subset of L

for x being Element of L holds {x} "/\" D is_<=_than x

proof end;

theorem :: YELLOW_4:53

for L being Semilattice

for X being Subset of L

for x being Element of L st ex_sup_of {x} "/\" X,L & ex_sup_of X,L holds

sup ({x} "/\" X) <= x "/\" (sup X)

for X being Subset of L

for x being Element of L st ex_sup_of {x} "/\" X,L & ex_sup_of X,L holds

sup ({x} "/\" X) <= x "/\" (sup X)

proof end;

theorem Th54: :: YELLOW_4:54

for L being non empty transitive antisymmetric complete RelStr

for A being Subset of L

for B being non empty Subset of L holds A is_>=_than inf (A "/\" B)

for A being Subset of L

for B being non empty Subset of L holds A is_>=_than inf (A "/\" B)

proof end;

theorem Th55: :: YELLOW_4:55

for L being transitive antisymmetric with_infima RelStr

for a, b being Element of L

for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds

a "/\" b is_<=_than A "/\" B

for a, b being Element of L

for A, B being Subset of L st a is_<=_than A & b is_<=_than B holds

a "/\" b is_<=_than A "/\" B

proof end;

theorem :: YELLOW_4:56

for L being transitive antisymmetric with_infima RelStr

for a, b being Element of L

for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds

a "/\" b is_>=_than A "/\" B

for a, b being Element of L

for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds

a "/\" b is_>=_than A "/\" B

proof end;

theorem :: YELLOW_4:57

for L being non empty complete Poset

for A, B being non empty Subset of L holds inf (A "/\" B) = (inf A) "/\" (inf B)

for A, B being non empty Subset of L holds inf (A "/\" B) = (inf A) "/\" (inf B)

proof end;

theorem :: YELLOW_4:58

for L being Semilattice

for x, y being Element of (InclPoset (Ids L))

for x1, y1 being Subset of L st x = x1 & y = y1 holds

x "/\" y = x1 "/\" y1

for x, y being Element of (InclPoset (Ids L))

for x1, y1 being Subset of L st x = x1 & y = y1 holds

x "/\" y = x1 "/\" y1

proof end;

theorem :: YELLOW_4:59

for L being antisymmetric with_infima RelStr

for X being Subset of L

for Y being non empty Subset of L holds X c= uparrow (X "/\" Y)

for X being Subset of L

for Y being non empty Subset of L holds X c= uparrow (X "/\" Y)

proof end;

theorem :: YELLOW_4:60

for L being non empty RelStr

for D being Subset of [:L,L:] holds union { X where X is Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D)

for D being Subset of [:L,L:] holds union { X where X is Subset of L : ex x being Element of L st

( X = {x} "/\" (proj2 D) & x in proj1 D ) } = (proj1 D) "/\" (proj2 D)

proof end;

theorem Th61: :: YELLOW_4:61

for L being transitive antisymmetric with_infima RelStr

for D1, D2 being Subset of L holds downarrow ((downarrow D1) "/\" (downarrow D2)) c= downarrow (D1 "/\" D2)

for D1, D2 being Subset of L holds downarrow ((downarrow D1) "/\" (downarrow D2)) c= downarrow (D1 "/\" D2)

proof end;

theorem :: YELLOW_4:62

for L being Semilattice

for D1, D2 being Subset of L holds downarrow ((downarrow D1) "/\" (downarrow D2)) = downarrow (D1 "/\" D2)

for D1, D2 being Subset of L holds downarrow ((downarrow D1) "/\" (downarrow D2)) = downarrow (D1 "/\" D2)

proof end;

theorem Th63: :: YELLOW_4:63

for L being transitive antisymmetric with_infima RelStr

for D1, D2 being Subset of L holds uparrow ((uparrow D1) "/\" (uparrow D2)) c= uparrow (D1 "/\" D2)

for D1, D2 being Subset of L holds uparrow ((uparrow D1) "/\" (uparrow D2)) c= uparrow (D1 "/\" D2)

proof end;

theorem :: YELLOW_4:64

for L being Semilattice

for D1, D2 being Subset of L holds uparrow ((uparrow D1) "/\" (uparrow D2)) = uparrow (D1 "/\" D2)

for D1, D2 being Subset of L holds uparrow ((uparrow D1) "/\" (uparrow D2)) = uparrow (D1 "/\" D2)

proof end;