:: by Adam Grabowski

::

:: Received January 17, 2013

:: Copyright (c) 2013-2019 Association of Mizar Users

registration
end;

theorem Th2: :: ROUGHS_2:2

for R being non empty 1-sorted

for X being Subset of R holds { x where x is Element of R : {} c= X } = [#] R

for X being Subset of R holds { x where x is Element of R : {} c= X } = [#] R

proof end;

theorem Th3: :: ROUGHS_2:3

for R being 1-sorted

for X being Subset of R holds { x where x is Element of R : {} meets X } = {} R

for X being Subset of R holds { x where x is Element of R : {} meets X } = {} R

proof end;

definition

let R be Relation;

let X be set ;

end;
let X be set ;

pred R is_serial_in X means :Def1: :: ROUGHS_2:def 1

for x being object st x in X holds

ex y being object st

( y in X & [x,y] in R );

for x being object st x in X holds

ex y being object st

( y in X & [x,y] in R );

:: deftheorem Def1 defines is_serial_in ROUGHS_2:def 1 :

for R being Relation

for X being set holds

( R is_serial_in X iff for x being object st x in X holds

ex y being object st

( y in X & [x,y] in R ) );

for R being Relation

for X being set holds

( R is_serial_in X iff for x being object st x in X holds

ex y being object st

( y in X & [x,y] in R ) );

:: deftheorem defines serial ROUGHS_2:def 2 :

for R being Relation holds

( R is serial iff R is_serial_in field R );

for R being Relation holds

( R is serial iff R is_serial_in field R );

:: deftheorem Def3 defines serial ROUGHS_2:def 3 :

for R being RelStr holds

( R is serial iff the InternalRel of R is_serial_in the carrier of R );

for R being RelStr holds

( R is serial iff the InternalRel of R is_serial_in the carrier of R );

Lm1: for R being RelStr st the InternalRel of R is_reflexive_in the carrier of R holds

R is serial

proof end;

registration

coherence

for b_{1} being RelStr st b_{1} is reflexive holds

b_{1} is serial
by Lm1, ORDERS_2:def 2;

end;
for b

b

definition

let R be non empty RelStr ;

( R is serial iff for x being Element of R ex y being Element of R st x <= y )

end;
redefine attr R is serial means :: ROUGHS_2:def 4

for x being Element of R ex y being Element of R st x <= y;

compatibility for x being Element of R ex y being Element of R st x <= y;

( R is serial iff for x being Element of R ex y being Element of R st x <= y )

proof end;

:: deftheorem defines serial ROUGHS_2:def 4 :

for R being non empty RelStr holds

( R is serial iff for x being Element of R ex y being Element of R st x <= y );

for R being non empty RelStr holds

( R is serial iff for x being Element of R ex y being Element of R st x <= y );

registration

coherence

for b_{1} being RelStr st b_{1} is total holds

b_{1} is serial

for b_{1} being RelStr st b_{1} is serial holds

b_{1} is total

end;
for b

b

proof end;

coherence for b

b

proof end;

Lm2: for R being non empty serial RelStr

for x being Element of R holds Class ( the InternalRel of R,x) <> {}

proof end;

registration

let R be non empty serial RelStr ;

let x be Element of R;

coherence

not Class ( the InternalRel of R,x) is empty by Lm2;

end;
let x be Element of R;

coherence

not Class ( the InternalRel of R,x) is empty by Lm2;

:: Reflexive relations

theorem Th4: :: ROUGHS_2:4

for R being non empty reflexive RelStr

for x being Element of R holds x in Class ( the InternalRel of R,x)

for x being Element of R holds x in Class ( the InternalRel of R,x)

proof end;

registration

let R be non empty reflexive RelStr ;

let x be Element of R;

coherence

not Class ( the InternalRel of R,x) is empty ;

end;
let x be Element of R;

coherence

not Class ( the InternalRel of R,x) is empty ;

:: Mediate relations

:: deftheorem Def5 defines is_mediate_in ROUGHS_2:def 5 :

for R being Relation

for X being set holds

( R is_mediate_in X iff for x, y being object st x in X & y in X & [x,y] in R holds

ex z being object st

( z in X & [x,z] in R & [z,y] in R ) );

for R being Relation

for X being set holds

( R is_mediate_in X iff for x, y being object st x in X & y in X & [x,y] in R holds

ex z being object st

( z in X & [x,z] in R & [z,y] in R ) );

definition
end;

:: deftheorem defines mediate ROUGHS_2:def 6 :

for R being Relation holds

( R is mediate iff R is_mediate_in field R );

for R being Relation holds

( R is mediate iff R is_mediate_in field R );

definition

let R be RelStr ;

end;
attr R is mediate means :Def7: :: ROUGHS_2:def 7

the InternalRel of R is_mediate_in the carrier of R;

the InternalRel of R is_mediate_in the carrier of R;

:: deftheorem Def7 defines mediate ROUGHS_2:def 7 :

for R being RelStr holds

( R is mediate iff the InternalRel of R is_mediate_in the carrier of R );

for R being RelStr holds

( R is mediate iff the InternalRel of R is_mediate_in the carrier of R );

registration
end;

theorem Th5: :: ROUGHS_2:5

for R being non empty RelStr

for a, b being Element of R st a in UAp {b} holds

[a,b] in the InternalRel of R

for a, b being Element of R st a in UAp {b} holds

[a,b] in the InternalRel of R

proof end;

definition
end;

:: deftheorem defines Uap ROUGHS_2:def 8 :

for R being non empty RelStr

for X being Subset of R holds Uap X = (LAp (X `)) ` ;

for R being non empty RelStr

for X being Subset of R holds Uap X = (LAp (X `)) ` ;

definition
end;

:: deftheorem defines Lap ROUGHS_2:def 9 :

for R being non empty RelStr

for X being Subset of R holds Lap X = (UAp (X `)) ` ;

for R being non empty RelStr

for X being Subset of R holds Lap X = (UAp (X `)) ` ;

theorem Th6: :: ROUGHS_2:6

for R being non empty RelStr

for X being Subset of R

for x being object st x in LAp X holds

Class ( the InternalRel of R,x) c= X

for X being Subset of R

for x being object st x in LAp X holds

Class ( the InternalRel of R,x) c= X

proof end;

theorem Th7: :: ROUGHS_2:7

for R being non empty RelStr

for X being Subset of R

for x being set st x in UAp X holds

Class ( the InternalRel of R,x) meets X

for X being Subset of R

for x being set st x in UAp X holds

Class ( the InternalRel of R,x) meets X

proof end;

registration
end;

definition

let R be non empty RelStr ;

ex b_{1} being Function of (bool the carrier of R),(bool the carrier of R) st

for X being Subset of R holds b_{1} . X = LAp X

for b_{1}, b_{2} being Function of (bool the carrier of R),(bool the carrier of R) st ( for X being Subset of R holds b_{1} . X = LAp X ) & ( for X being Subset of R holds b_{2} . X = LAp X ) holds

b_{1} = b_{2}

ex b_{1} being Function of (bool the carrier of R),(bool the carrier of R) st

for X being Subset of R holds b_{1} . X = UAp X

for b_{1}, b_{2} being Function of (bool the carrier of R),(bool the carrier of R) st ( for X being Subset of R holds b_{1} . X = UAp X ) & ( for X being Subset of R holds b_{2} . X = UAp X ) holds

b_{1} = b_{2}

end;
func LAp R -> Function of (bool the carrier of R),(bool the carrier of R) means :Def10: :: ROUGHS_2:def 10

for X being Subset of R holds it . X = LAp X;

existence for X being Subset of R holds it . X = LAp X;

ex b

for X being Subset of R holds b

proof end;

uniqueness for b

b

proof end;

func UAp R -> Function of (bool the carrier of R),(bool the carrier of R) means :Def11: :: ROUGHS_2:def 11

for X being Subset of R holds it . X = UAp X;

existence for X being Subset of R holds it . X = UAp X;

ex b

for X being Subset of R holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines LAp ROUGHS_2:def 10 :

for R being non empty RelStr

for b_{2} being Function of (bool the carrier of R),(bool the carrier of R) holds

( b_{2} = LAp R iff for X being Subset of R holds b_{2} . X = LAp X );

for R being non empty RelStr

for b

( b

:: deftheorem Def11 defines UAp ROUGHS_2:def 11 :

for R being non empty RelStr

for b_{2} being Function of (bool the carrier of R),(bool the carrier of R) holds

( b_{2} = UAp R iff for X being Subset of R holds b_{2} . X = UAp X );

for R being non empty RelStr

for b

( b

definition
end;

:: deftheorem Def12 defines empty-preserving ROUGHS_2:def 12 :

for f being Function holds

( f is empty-preserving iff f . {} = {} );

for f being Function holds

( f is empty-preserving iff f . {} = {} );

:: deftheorem Def13 defines universe-preserving ROUGHS_2:def 13 :

for A being set

for f being Function of (bool A),(bool A) holds

( f is universe-preserving iff f . A = A );

for A being set

for f being Function of (bool A),(bool A) holds

( f is universe-preserving iff f . A = A );

registration

let A be non empty set ;

coherence

for b_{1} being Function of (bool A),(bool A) st b_{1} = id (bool A) holds

( b_{1} is empty-preserving & b_{1} is universe-preserving )

end;
coherence

for b

( b

proof end;

registration

let A be non empty set ;

ex b_{1} being Function of (bool A),(bool A) st

( b_{1} is empty-preserving & b_{1} is universe-preserving )

end;
cluster non empty Relation-like bool A -defined bool A -valued Function-like total V29( bool A, bool A) empty-preserving universe-preserving for Element of bool [:(bool A),(bool A):];

existence ex b

( b

proof end;

definition

let X be set ;

let f be Function of (bool X),(bool X);

ex b_{1} being Function of (bool X),(bool X) st

for x being Subset of X holds b_{1} . x = (f . (x `)) `

for b_{1}, b_{2} being Function of (bool X),(bool X) st ( for x being Subset of X holds b_{1} . x = (f . (x `)) ` ) & ( for x being Subset of X holds b_{2} . x = (f . (x `)) ` ) holds

b_{1} = b_{2}

end;
let f be Function of (bool X),(bool X);

func Flip f -> Function of (bool X),(bool X) means :Def14: :: ROUGHS_2:def 14

for x being Subset of X holds it . x = (f . (x `)) ` ;

existence for x being Subset of X holds it . x = (f . (x `)) ` ;

ex b

for x being Subset of X holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def14 defines Flip ROUGHS_2:def 14 :

for X being set

for f, b_{3} being Function of (bool X),(bool X) holds

( b_{3} = Flip f iff for x being Subset of X holds b_{3} . x = (f . (x `)) ` );

for X being set

for f, b

( b

theorem :: ROUGHS_2:21

for X being set

for f being Function of (bool X),(bool X) st ( for A, B being Subset of X holds f . (A \/ B) = (f . A) \/ (f . B) ) holds

for A, B being Subset of X holds (Flip f) . (A /\ B) = ((Flip f) . A) /\ ((Flip f) . B)

for f being Function of (bool X),(bool X) st ( for A, B being Subset of X holds f . (A \/ B) = (f . A) \/ (f . B) ) holds

for A, B being Subset of X holds (Flip f) . (A /\ B) = ((Flip f) . A) /\ ((Flip f) . B)

proof end;

theorem Th22: :: ROUGHS_2:22

for X being set

for f being Function of (bool X),(bool X) st ( for A, B being Subset of X holds f . (A /\ B) = (f . A) /\ (f . B) ) holds

for A, B being Subset of X holds (Flip f) . (A \/ B) = ((Flip f) . A) \/ ((Flip f) . B)

for f being Function of (bool X),(bool X) st ( for A, B being Subset of X holds f . (A /\ B) = (f . A) /\ (f . B) ) holds

for A, B being Subset of X holds (Flip f) . (A \/ B) = ((Flip f) . A) \/ ((Flip f) . B)

proof end;

registration

let A be non empty set ;

let f be universe-preserving Function of (bool A),(bool A);

coherence

Flip f is empty-preserving

end;
let f be universe-preserving Function of (bool A),(bool A);

coherence

Flip f is empty-preserving

proof end;

registration

let A be non empty set ;

let f be empty-preserving Function of (bool A),(bool A);

coherence

Flip f is universe-preserving

end;
let f be empty-preserving Function of (bool A),(bool A);

coherence

Flip f is universe-preserving

proof end;

theorem Th24: :: ROUGHS_2:24

for A being non empty set

for L, U being Function of (bool A),(bool A) st U = Flip L & ( for X being Subset of A holds L . (L . X) c= L . X ) holds

for X being Subset of A holds U . X c= U . (U . X)

for L, U being Function of (bool A),(bool A) st U = Flip L & ( for X being Subset of A holds L . (L . X) c= L . X ) holds

for X being Subset of A holds U . X c= U . (U . X)

proof end;

definition

let T be TopSpace;

ex b_{1} being Function of (bool the carrier of T),(bool the carrier of T) st

for X being Subset of T holds b_{1} . X = Cl X

for b_{1}, b_{2} being Function of (bool the carrier of T),(bool the carrier of T) st ( for X being Subset of T holds b_{1} . X = Cl X ) & ( for X being Subset of T holds b_{2} . X = Cl X ) holds

b_{1} = b_{2}

ex b_{1} being Function of (bool the carrier of T),(bool the carrier of T) st

for X being Subset of T holds b_{1} . X = Int X

for b_{1}, b_{2} being Function of (bool the carrier of T),(bool the carrier of T) st ( for X being Subset of T holds b_{1} . X = Int X ) & ( for X being Subset of T holds b_{2} . X = Int X ) holds

b_{1} = b_{2}

end;
func ClMap T -> Function of (bool the carrier of T),(bool the carrier of T) means :Def15: :: ROUGHS_2:def 15

for X being Subset of T holds it . X = Cl X;

existence for X being Subset of T holds it . X = Cl X;

ex b

for X being Subset of T holds b

proof end;

uniqueness for b

b

proof end;

func IntMap T -> Function of (bool the carrier of T),(bool the carrier of T) means :Def16: :: ROUGHS_2:def 16

for X being Subset of T holds it . X = Int X;

existence for X being Subset of T holds it . X = Int X;

ex b

for X being Subset of T holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def15 defines ClMap ROUGHS_2:def 15 :

for T being TopSpace

for b_{2} being Function of (bool the carrier of T),(bool the carrier of T) holds

( b_{2} = ClMap T iff for X being Subset of T holds b_{2} . X = Cl X );

for T being TopSpace

for b

( b

:: deftheorem Def16 defines IntMap ROUGHS_2:def 16 :

for T being TopSpace

for b_{2} being Function of (bool the carrier of T),(bool the carrier of T) holds

( b_{2} = IntMap T iff for X being Subset of T holds b_{2} . X = Int X );

for T being TopSpace

for b

( b

definition
end;

:: deftheorem defines closed-valued ROUGHS_2:def 17 :

for T being TopSpace

for f being Function of (bool the carrier of T),(bool the carrier of T) holds

( f is closed-valued iff for X being Subset of T holds f . X is closed );

for T being TopSpace

for f being Function of (bool the carrier of T),(bool the carrier of T) holds

( f is closed-valued iff for X being Subset of T holds f . X is closed );

:: deftheorem defines open-valued ROUGHS_2:def 18 :

for T being TopSpace

for f being Function of (bool the carrier of T),(bool the carrier of T) holds

( f is open-valued iff for X being Subset of T holds f . X is open );

for T being TopSpace

for f being Function of (bool the carrier of T),(bool the carrier of T) holds

( f is open-valued iff for X being Subset of T holds f . X is open );

registration

let T be TopSpace;

coherence

ClMap T is closed-valued

IntMap T is open-valued

end;
coherence

ClMap T is closed-valued

proof end;

coherence IntMap T is open-valued

proof end;

registration

let T be TopSpace;

ex b_{1} being Function of (bool the carrier of T),(bool the carrier of T) st b_{1} is closed-valued

ex b_{1} being Function of (bool the carrier of T),(bool the carrier of T) st b_{1} is open-valued

end;
cluster non empty Relation-like bool the carrier of T -defined bool the carrier of T -valued Function-like total V29( bool the carrier of T, bool the carrier of T) closed-valued for Element of bool [:(bool the carrier of T),(bool the carrier of T):];

existence ex b

proof end;

cluster non empty Relation-like bool the carrier of T -defined bool the carrier of T -valued Function-like total V29( bool the carrier of T, bool the carrier of T) open-valued for Element of bool [:(bool the carrier of T),(bool the carrier of T):];

existence ex b

proof end;

registration

let T be non empty TopSpace;

coherence

( ClMap T is empty-preserving & ClMap T is universe-preserving )

( IntMap T is empty-preserving & IntMap T is universe-preserving )

end;
coherence

( ClMap T is empty-preserving & ClMap T is universe-preserving )

proof end;

coherence ( IntMap T is empty-preserving & IntMap T is universe-preserving )

proof end;

:: General Finite Relations

theorem Th29: :: ROUGHS_2:29

for A being non empty finite set

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite RelStr st

( the carrier of R = A & U = UAp R )

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite RelStr st

( the carrier of R = A & U = UAp R )

proof end;

theorem Th30: :: ROUGHS_2:30

for A being non empty finite set

for L being Function of (bool A),(bool A) st L . A = A & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite RelStr st

( the carrier of R = A & L = LAp R )

for L being Function of (bool A),(bool A) st L . A = A & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite RelStr st

( the carrier of R = A & L = LAp R )

proof end;

:: Serial Relations

theorem Th31: :: ROUGHS_2:31

for A being non empty finite set

for L being Function of (bool A),(bool A) st L . A = A & L . {} = {} & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty serial RelStr st

( the carrier of R = A & L = LAp R )

for L being Function of (bool A),(bool A) st L . A = A & L . {} = {} & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty serial RelStr st

( the carrier of R = A & L = LAp R )

proof end;

theorem Th32: :: ROUGHS_2:32

for A being non empty finite set

for U being Function of (bool A),(bool A) st U . A = A & U . {} = {} & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite serial RelStr st

( the carrier of R = A & U = UAp R )

for U being Function of (bool A),(bool A) st U . A = A & U . {} = {} & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite serial RelStr st

( the carrier of R = A & U = UAp R )

proof end;

theorem Th33: :: ROUGHS_2:33

for A being non empty finite set

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds L . X c= (L . (X `)) ` ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite serial RelStr st

( the carrier of R = A & L = LAp R )

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds L . X c= (L . (X `)) ` ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite serial RelStr st

( the carrier of R = A & L = LAp R )

proof end;

theorem Th34: :: ROUGHS_2:34

for A being non empty finite set

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds (U . (X `)) ` c= U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty serial RelStr st

( the carrier of R = A & U = UAp R )

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds (U . (X `)) ` c= U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty serial RelStr st

( the carrier of R = A & U = UAp R )

proof end;

:: Reflexive binary relations

theorem Th37: :: ROUGHS_2:37

for A being non empty finite set

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds X c= U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite reflexive RelStr st

( the carrier of R = A & U = UAp R )

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds X c= U . X ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite reflexive RelStr st

( the carrier of R = A & U = UAp R )

proof end;

theorem :: ROUGHS_2:38

for A being non empty finite set

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds L . X c= X ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite reflexive RelStr st

( the carrier of R = A & L = LAp R )

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds L . X c= X ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite reflexive RelStr st

( the carrier of R = A & L = LAp R )

proof end;

:: Mediate Relations

theorem Th41: :: ROUGHS_2:41

for A being non empty finite set

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds U . X c= U . (U . X) ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite mediate RelStr st

( the carrier of R = A & U = UAp R )

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X being Subset of A holds U . X c= U . (U . X) ) & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

ex R being non empty finite mediate RelStr st

( the carrier of R = A & U = UAp R )

proof end;

theorem :: ROUGHS_2:42

for A being non empty finite set

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds L . (L . X) c= L . X ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite mediate RelStr st

( the carrier of R = A & L = LAp R )

for L being Function of (bool A),(bool A) st L . A = A & ( for X being Subset of A holds L . (L . X) c= L . X ) & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

ex R being non empty finite mediate RelStr st

( the carrier of R = A & L = LAp R )

proof end;

:: Corollaries

theorem :: ROUGHS_2:43

for A being non empty finite set

for L being Function of (bool A),(bool A) st L . A = A & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

( ( for X being Subset of A holds L . X c= (L . (X `)) ` ) iff L . {} = {} )

for L being Function of (bool A),(bool A) st L . A = A & ( for X, Y being Subset of A holds L . (X /\ Y) = (L . X) /\ (L . Y) ) holds

( ( for X being Subset of A holds L . X c= (L . (X `)) ` ) iff L . {} = {} )

proof end;

theorem :: ROUGHS_2:44

for A being non empty finite set

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

( ( for X being Subset of A holds (U . (X `)) ` c= U . X ) iff U . A = A )

for U being Function of (bool A),(bool A) st U . {} = {} & ( for X, Y being Subset of A holds U . (X \/ Y) = (U . X) \/ (U . Y) ) holds

( ( for X being Subset of A holds (U . (X `)) ` c= U . X ) iff U . A = A )

proof end;