:: by Library Committee

::

:: Received April 08, 2002

:: Copyright (c) 2002 Association of Mizar Users

begin

theorem Th1: :: XBOOLE_1:1

proof end;

theorem Th2: :: XBOOLE_1:2

proof end;

theorem Th3: :: XBOOLE_1:3

proof end;

theorem Th4: :: XBOOLE_1:4

proof end;

theorem :: XBOOLE_1:5

proof end;

theorem :: XBOOLE_1:6

proof end;

theorem Th7: :: XBOOLE_1:7

proof end;

theorem Th8: :: XBOOLE_1:8

proof end;

theorem :: XBOOLE_1:9

proof end;

theorem :: XBOOLE_1:10

proof end;

theorem :: XBOOLE_1:11

proof end;

theorem Th12: :: XBOOLE_1:12

proof end;

theorem :: XBOOLE_1:13

proof end;

theorem :: XBOOLE_1:14

for Y, X, Z being set st Y c= X & Z c= X & ( for V being set st Y c= V & Z c= V holds

X c= V ) holds

X = Y \/ Z

X c= V ) holds

X = Y \/ Z

proof end;

theorem :: XBOOLE_1:15

theorem Th16: :: XBOOLE_1:16

proof end;

theorem Th17: :: XBOOLE_1:17

proof end;

theorem :: XBOOLE_1:18

proof end;

theorem Th19: :: XBOOLE_1:19

proof end;

theorem :: XBOOLE_1:20

for X, Y, Z being set st X c= Y & X c= Z & ( for V being set st V c= Y & V c= Z holds

V c= X ) holds

X = Y /\ Z

V c= X ) holds

X = Y /\ Z

proof end;

theorem :: XBOOLE_1:21

proof end;

theorem Th22: :: XBOOLE_1:22

proof end;

theorem Th23: :: XBOOLE_1:23

proof end;

theorem Th24: :: XBOOLE_1:24

proof end;

theorem :: XBOOLE_1:25

proof end;

theorem Th26: :: XBOOLE_1:26

proof end;

theorem :: XBOOLE_1:27

proof end;

theorem Th28: :: XBOOLE_1:28

proof end;

theorem :: XBOOLE_1:29

proof end;

theorem :: XBOOLE_1:30

proof end;

theorem :: XBOOLE_1:31

proof end;

Lm1: for X, Y being set holds

( X \ Y = {} iff X c= Y )

proof end;

theorem :: XBOOLE_1:32

proof end;

theorem Th33: :: XBOOLE_1:33

proof end;

theorem Th34: :: XBOOLE_1:34

proof end;

Lm2: for X, Y, Z being set holds X \ (Y /\ Z) = (X \ Y) \/ (X \ Z)

proof end;

theorem :: XBOOLE_1:35

proof end;

theorem Th36: :: XBOOLE_1:36

proof end;

theorem :: XBOOLE_1:37

theorem :: XBOOLE_1:38

proof end;

theorem Th39: :: XBOOLE_1:39

proof end;

theorem :: XBOOLE_1:40

proof end;

theorem Th41: :: XBOOLE_1:41

proof end;

theorem Th42: :: XBOOLE_1:42

proof end;

theorem :: XBOOLE_1:43

proof end;

theorem :: XBOOLE_1:44

proof end;

theorem :: XBOOLE_1:45

proof end;

theorem :: XBOOLE_1:46

proof end;

theorem Th47: :: XBOOLE_1:47

proof end;

theorem :: XBOOLE_1:48

proof end;

theorem Th49: :: XBOOLE_1:49

proof end;

theorem Th50: :: XBOOLE_1:50

proof end;

theorem Th51: :: XBOOLE_1:51

proof end;

theorem Th52: :: XBOOLE_1:52

proof end;

theorem :: XBOOLE_1:53

proof end;

theorem :: XBOOLE_1:54

theorem Th55: :: XBOOLE_1:55

proof end;

Lm3: for X, Y, Z being set st X c= Y & Y c< Z holds

X c< Z

proof end;

theorem :: XBOOLE_1:56

proof end;

theorem :: XBOOLE_1:57

theorem :: XBOOLE_1:58

proof end;

theorem :: XBOOLE_1:59

theorem Th60: :: XBOOLE_1:60

proof end;

theorem :: XBOOLE_1:61

proof end;

theorem :: XBOOLE_1:62

proof end;

theorem Th63: :: XBOOLE_1:63

proof end;

theorem :: XBOOLE_1:64

proof end;

theorem :: XBOOLE_1:65

proof end;

theorem :: XBOOLE_1:66

proof end;

theorem :: XBOOLE_1:67

proof end;

theorem :: XBOOLE_1:68

proof end;

theorem :: XBOOLE_1:69

proof end;

theorem Th70: :: XBOOLE_1:70

proof end;

theorem :: XBOOLE_1:71

proof end;

theorem :: XBOOLE_1:72

proof end;

theorem :: XBOOLE_1:73

proof end;

theorem Th74: :: XBOOLE_1:74

proof end;

theorem :: XBOOLE_1:75

proof end;

theorem :: XBOOLE_1:76

proof end;

theorem :: XBOOLE_1:77

proof end;

theorem :: XBOOLE_1:78

proof end;

theorem Th79: :: XBOOLE_1:79

proof end;

theorem :: XBOOLE_1:80

proof end;

theorem :: XBOOLE_1:81

proof end;

theorem :: XBOOLE_1:82

proof end;

theorem Th83: :: XBOOLE_1:83

proof end;

theorem :: XBOOLE_1:84

proof end;

theorem :: XBOOLE_1:85

proof end;

theorem Th86: :: XBOOLE_1:86

proof end;

theorem :: XBOOLE_1:87

proof end;

theorem Th88: :: XBOOLE_1:88

proof end;

theorem Th89: :: XBOOLE_1:89

proof end;

theorem :: XBOOLE_1:90

proof end;

theorem :: XBOOLE_1:91

proof end;

theorem :: XBOOLE_1:92

theorem Th93: :: XBOOLE_1:93

proof end;

Lm4: for X, Y being set holds X /\ Y misses X \+\ Y

proof end;

Lm5: for X, Y being set holds X \+\ Y = (X \/ Y) \ (X /\ Y)

proof end;

theorem :: XBOOLE_1:94

proof end;

theorem :: XBOOLE_1:95

proof end;

theorem :: XBOOLE_1:96

theorem :: XBOOLE_1:97

theorem :: XBOOLE_1:98

proof end;

theorem :: XBOOLE_1:99

proof end;

theorem :: XBOOLE_1:100

proof end;

theorem :: XBOOLE_1:101

theorem :: XBOOLE_1:102

proof end;

theorem :: XBOOLE_1:103

theorem :: XBOOLE_1:104

proof end;

begin

theorem :: XBOOLE_1:105

proof end;

theorem Th106: :: XBOOLE_1:106

proof end;

theorem :: XBOOLE_1:107

proof end;

theorem :: XBOOLE_1:108

proof end;

theorem Th109: :: XBOOLE_1:109

proof end;

theorem :: XBOOLE_1:110

proof end;

theorem Th111: :: XBOOLE_1:111

proof end;

theorem :: XBOOLE_1:112

proof end;

theorem :: XBOOLE_1:113

proof end;

theorem :: XBOOLE_1:114

proof end;

theorem :: XBOOLE_1:115

proof end;

theorem :: XBOOLE_1:116

proof end;

theorem :: XBOOLE_1:117

proof end;