:: Miscellaneous Facts about Relation Structure
:: by Agnieszka Julia Marasik
::
:: Received November 8, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users


theorem :: YELLOW_5:1
for L being reflexive antisymmetric with_suprema RelStr
for a being Element of L holds a "\/" a = a
proof end;

theorem Th2: :: YELLOW_5:2
for L being reflexive antisymmetric with_infima RelStr
for a being Element of L holds a "/\" a = a
proof end;

theorem :: YELLOW_5:3
for L being transitive antisymmetric with_suprema RelStr
for a, b, c being Element of L st a "\/" b <= c holds
a <= c
proof end;

theorem :: YELLOW_5:4
for L being transitive antisymmetric with_infima RelStr
for a, b, c being Element of L st c <= a "/\" b holds
c <= a
proof end;

theorem :: YELLOW_5:5
for L being transitive antisymmetric with_suprema with_infima RelStr
for a, b, c being Element of L holds a "/\" b <= a "\/" c
proof end;

theorem Th6: :: YELLOW_5:6
for L being transitive antisymmetric with_infima RelStr
for a, b, c being Element of L st a <= b holds
a "/\" c <= b "/\" c
proof end;

theorem Th7: :: YELLOW_5:7
for L being transitive antisymmetric with_suprema RelStr
for a, b, c being Element of L st a <= b holds
a "\/" c <= b "\/" c
proof end;

theorem Th8: :: YELLOW_5:8
for L being sup-Semilattice
for a, b being Element of L st a <= b holds
a "\/" b = b
proof end;

theorem Th9: :: YELLOW_5:9
for L being sup-Semilattice
for a, b, c being Element of L st a <= c & b <= c holds
a "\/" b <= c
proof end;

theorem Th10: :: YELLOW_5:10
for L being Semilattice
for a, b being Element of L st b <= a holds
a "/\" b = b
proof end;

theorem Th11: :: YELLOW_5:11
for L being Boolean LATTICE
for x, y being Element of L holds
( y is_a_complement_of x iff y = 'not' x )
proof end;

definition
let L be non empty RelStr ;
let a, b be Element of L;
func a \ b -> Element of L equals :: YELLOW_5:def 1
a "/\" ('not' b);
correctness
coherence
a "/\" ('not' b) is Element of L;
;
end;

:: deftheorem defines \ YELLOW_5:def 1 :
for L being non empty RelStr
for a, b being Element of L holds a \ b = a "/\" ('not' b);

definition
let L be non empty RelStr ;
let a, b be Element of L;
func a \+\ b -> Element of L equals :: YELLOW_5:def 2
(a \ b) "\/" (b \ a);
correctness
coherence
(a \ b) "\/" (b \ a) is Element of L;
;
end;

:: deftheorem defines \+\ YELLOW_5:def 2 :
for L being non empty RelStr
for a, b being Element of L holds a \+\ b = (a \ b) "\/" (b \ a);

definition
let L be antisymmetric with_suprema with_infima RelStr ;
let a, b be Element of L;
:: original: \+\
redefine func a \+\ b -> Element of L;
commutativity
for a, b being Element of L holds a \+\ b = b \+\ a
proof end;
end;

definition
let L be non empty RelStr ;
let a, b be Element of L;
pred a meets b means :: YELLOW_5:def 3
a "/\" b <> Bottom L;
end;

:: deftheorem defines meets YELLOW_5:def 3 :
for L being non empty RelStr
for a, b being Element of L holds
( a meets b iff a "/\" b <> Bottom L );

notation
let L be non empty RelStr ;
let a, b be Element of L;
antonym a misses b for a meets b;
end;

notation
let L be antisymmetric with_infima RelStr ;
let a, b be Element of L;
antonym a misses b for a meets b;
end;

definition
let L be antisymmetric with_infima RelStr ;
let a, b be Element of L;
:: original: meets
redefine pred a meets b;
symmetry
for a, b being Element of L st (L,b1,b2) holds
(L,b2,b1)
proof end;
end;

theorem :: YELLOW_5:12
for L being transitive antisymmetric with_suprema with_infima RelStr
for a, b, c being Element of L st a <= c holds
a \ b <= c
proof end;

theorem :: YELLOW_5:13
for L being transitive antisymmetric with_suprema with_infima RelStr
for a, b, c being Element of L st a <= b holds
a \ c <= b \ c by Th6;

theorem :: YELLOW_5:14
for L being LATTICE
for a, b, c being Element of L st a \ b <= c & b \ a <= c holds
a \+\ b <= c by Th9;

theorem :: YELLOW_5:15
for L being LATTICE
for a being Element of L holds
( a meets a iff a <> Bottom L ) by Th2;

theorem :: YELLOW_5:16
for L being transitive antisymmetric with_infima RelStr st L is distributive holds
for a, b, c being Element of L st (a "/\" b) "\/" (a "/\" c) = a holds
a <= b "\/" c
proof end;

theorem Th17: :: YELLOW_5:17
for L being LATTICE st L is distributive holds
for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
proof end;

theorem :: YELLOW_5:18
for L being LATTICE st L is distributive holds
for a, b, c being Element of L holds (a "\/" b) \ c = (a \ c) "\/" (b \ c)
proof end;

theorem Th19: :: YELLOW_5:19
for L being non empty antisymmetric lower-bounded RelStr
for a being Element of L st a <= Bottom L holds
a = Bottom L
proof end;

theorem :: YELLOW_5:20
for L being lower-bounded Semilattice
for a, b, c being Element of L st a <= b & a <= c & b "/\" c = Bottom L holds
a = Bottom L
proof end;

theorem :: YELLOW_5:21
for L being antisymmetric with_suprema lower-bounded RelStr
for a, b being Element of L st a "\/" b = Bottom L holds
( a = Bottom L & b = Bottom L )
proof end;

theorem :: YELLOW_5:22
for L being transitive antisymmetric with_infima lower-bounded RelStr
for a, b, c being Element of L st a <= b & b "/\" c = Bottom L holds
a "/\" c = Bottom L
proof end;

theorem :: YELLOW_5:23
for L being lower-bounded Semilattice
for a being Element of L holds (Bottom L) \ a = Bottom L
proof end;

theorem :: YELLOW_5:24
for L being transitive antisymmetric with_infima lower-bounded RelStr
for a, b, c being Element of L st a meets b & b <= c holds
a meets c
proof end;

theorem Th25: :: YELLOW_5:25
for L being antisymmetric with_infima lower-bounded RelStr
for a being Element of L holds a "/\" (Bottom L) = Bottom L
proof end;

theorem :: YELLOW_5:26
for L being transitive antisymmetric with_suprema with_infima lower-bounded RelStr
for a, b, c being Element of L st a meets b "/\" c holds
a meets b
proof end;

theorem :: YELLOW_5:27
for L being transitive antisymmetric with_suprema with_infima lower-bounded RelStr
for a, b, c being Element of L st a meets b \ c holds
a meets b
proof end;

theorem :: YELLOW_5:28
for L being transitive antisymmetric with_infima lower-bounded RelStr
for a being Element of L holds a misses Bottom L by Th25;

theorem :: YELLOW_5:29
for L being transitive antisymmetric with_infima lower-bounded RelStr
for a, b, c being Element of L st a misses c & b <= c holds
a misses b
proof end;

theorem :: YELLOW_5:30
for L being transitive antisymmetric with_infima lower-bounded RelStr
for a, b, c being Element of L st ( a misses b or a misses c ) holds
a misses b "/\" c
proof end;

theorem :: YELLOW_5:31
for L being lower-bounded LATTICE
for a, b, c being Element of L st a <= b & a <= c & b misses c holds
a = Bottom L
proof end;

theorem :: YELLOW_5:32
for L being transitive antisymmetric with_infima lower-bounded RelStr
for a, b, c being Element of L st a misses b holds
a "/\" c misses b "/\" c
proof end;

theorem :: YELLOW_5:33
for L being non empty Boolean RelStr
for a, b, c being Element of L holds ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a)
proof end;

theorem Th34: :: YELLOW_5:34
for L being non empty Boolean RelStr
for a being Element of L holds
( a "/\" ('not' a) = Bottom L & a "\/" ('not' a) = Top L )
proof end;

theorem :: YELLOW_5:35
for L being non empty Boolean RelStr
for a, b, c being Element of L st a \ b <= c holds
a <= b "\/" c
proof end;

theorem Th36: :: YELLOW_5:36
for L being non empty Boolean RelStr
for a, b being Element of L holds
( 'not' (a "\/" b) = ('not' a) "/\" ('not' b) & 'not' (a "/\" b) = ('not' a) "\/" ('not' b) )
proof end;

theorem Th37: :: YELLOW_5:37
for L being non empty Boolean RelStr
for a, b being Element of L st a <= b holds
'not' b <= 'not' a
proof end;

theorem :: YELLOW_5:38
for L being non empty Boolean RelStr
for a, b, c being Element of L st a <= b holds
c \ b <= c \ a
proof end;

theorem :: YELLOW_5:39
for L being non empty Boolean RelStr
for a, b, c, d being Element of L st a <= b & c <= d holds
a \ d <= b \ c
proof end;

theorem :: YELLOW_5:40
for L being non empty Boolean RelStr
for a, b, c being Element of L st a <= b "\/" c holds
( a \ b <= c & a \ c <= b )
proof end;

theorem :: YELLOW_5:41
for L being non empty Boolean RelStr
for a, b being Element of L holds
( 'not' a <= 'not' (a "/\" b) & 'not' b <= 'not' (a "/\" b) )
proof end;

theorem :: YELLOW_5:42
for L being non empty Boolean RelStr
for a, b being Element of L holds
( 'not' (a "\/" b) <= 'not' a & 'not' (a "\/" b) <= 'not' b )
proof end;

theorem :: YELLOW_5:43
for L being non empty Boolean RelStr
for a, b being Element of L st a <= b \ a holds
a = Bottom L
proof end;

theorem :: YELLOW_5:44
for L being non empty Boolean RelStr
for a, b being Element of L st a <= b holds
b = a "\/" (b \ a)
proof end;

theorem :: YELLOW_5:45
for L being non empty Boolean RelStr
for a, b being Element of L holds
( a \ b = Bottom L iff a <= b )
proof end;

theorem :: YELLOW_5:46
for L being non empty Boolean RelStr
for a, b, c being Element of L st a <= b "\/" c & a "/\" c = Bottom L holds
a <= b
proof end;

theorem :: YELLOW_5:47
for L being non empty Boolean RelStr
for a, b being Element of L holds a "\/" b = (a \ b) "\/" b
proof end;

theorem :: YELLOW_5:48
for L being non empty Boolean RelStr
for a, b being Element of L holds a \ (a "\/" b) = Bottom L
proof end;

theorem :: YELLOW_5:49
for L being non empty Boolean RelStr
for a, b being Element of L holds a \ (a "/\" b) = a \ b
proof end;

theorem :: YELLOW_5:50
for L being non empty Boolean RelStr
for a, b being Element of L holds (a \ b) "/\" b = Bottom L
proof end;

theorem :: YELLOW_5:51
for L being non empty Boolean RelStr
for a, b being Element of L holds a "\/" (b \ a) = a "\/" b
proof end;

theorem :: YELLOW_5:52
for L being non empty Boolean RelStr
for a, b being Element of L holds (a "/\" b) "\/" (a \ b) = a
proof end;

theorem :: YELLOW_5:53
for L being non empty Boolean RelStr
for a, b, c being Element of L holds a \ (b \ c) = (a \ b) "\/" (a "/\" c)
proof end;

theorem :: YELLOW_5:54
for L being non empty Boolean RelStr
for a, b being Element of L holds a \ (a \ b) = a "/\" b
proof end;

theorem :: YELLOW_5:55
for L being non empty Boolean RelStr
for a, b being Element of L holds (a "\/" b) \ b = a \ b
proof end;

theorem :: YELLOW_5:56
for L being non empty Boolean RelStr
for a, b being Element of L holds
( a "/\" b = Bottom L iff a \ b = a )
proof end;

theorem :: YELLOW_5:57
for L being non empty Boolean RelStr
for a, b, c being Element of L holds a \ (b "\/" c) = (a \ b) "/\" (a \ c)
proof end;

theorem :: YELLOW_5:58
for L being non empty Boolean RelStr
for a, b, c being Element of L holds a \ (b "/\" c) = (a \ b) "\/" (a \ c)
proof end;

theorem :: YELLOW_5:59
for L being non empty Boolean RelStr
for a, b, c being Element of L holds a "/\" (b \ c) = (a "/\" b) \ (a "/\" c)
proof end;

theorem :: YELLOW_5:60
for L being non empty Boolean RelStr
for a, b being Element of L holds (a "\/" b) \ (a "/\" b) = (a \ b) "\/" (b \ a)
proof end;

theorem :: YELLOW_5:61
for L being non empty Boolean RelStr
for a, b, c being Element of L holds (a \ b) \ c = a \ (b "\/" c)
proof end;

theorem Th62: :: YELLOW_5:62
for L being non empty Boolean RelStr holds 'not' (Bottom L) = Top L
proof end;

theorem :: YELLOW_5:63
for L being non empty Boolean RelStr holds 'not' (Top L) = Bottom L
proof end;

theorem :: YELLOW_5:64
for L being non empty Boolean RelStr
for a being Element of L holds a \ a = Bottom L by Th34;

theorem :: YELLOW_5:65
for L being non empty Boolean RelStr
for a being Element of L holds a \ (Bottom L) = a
proof end;

theorem :: YELLOW_5:66
for L being non empty Boolean RelStr
for a, b being Element of L holds 'not' (a \ b) = ('not' a) "\/" b
proof end;

theorem :: YELLOW_5:67
for L being non empty Boolean RelStr
for a, b being Element of L holds a "/\" b misses a \ b
proof end;

theorem :: YELLOW_5:68
for L being non empty Boolean RelStr
for a, b being Element of L holds a \ b misses b
proof end;

theorem :: YELLOW_5:69
for L being non empty Boolean RelStr
for a, b being Element of L st a misses b holds
(a "\/" b) \ b = a
proof end;