:: SETFAM_1 semantic presentation

begin


definition
let X be set ;
func meet X ->  set  means :Def1: :: SETFAM_1:def 1
 for x being set holds
( x in it iff for Y being set st Y in X holds
x in Y ) if X <> {}
otherwise it = {} ;
existence
 ( ( X <> {} implies ex b1 being set st
for x being set holds
( x in b1 iff for Y being set st Y in X holds
x in Y ) ) & ( not X <> {} implies ex b1 being set st b1 = {} ) )
proof
thus  ( X <> {} implies ex Z1 being set st
for x being set holds
( x in Z1 iff for Z being set st Z in X holds
x in Z ) ) ::_thesis: ( not X <> {} implies ex b1 being set st b1 = {} )
proof
defpred S1[ set ] means  for Z being set st Z in X holds
$1 in Z;
assume A1: X <> {} ; ::_thesis: ex Z1 being set st
for x being set holds
( x in Z1 iff for Z being set st Z in X holds
x in Z )
consider Y being set  such that
A2: for x being set holds
( x in Y iff ( x in union X & S1[x] ) ) from XBOOLE_0:sch_1();
take  Y ; ::_thesis: for x being set holds
( x in Y iff for Z being set st Z in X holds
x in Z )
 for x being set st ( for Z being set st Z in X holds
x in Z ) holds
x in Y
proof
set y = the Element of X;
let x be set ; ::_thesis: ( ( for Z being set st Z in X holds
x in Z ) implies x in Y )
assume A3: for Z being set st Z in X holds
x in Z ; ::_thesis: x in Y
 x in the Element of X by A1, A3;
then  x in union X by A1, TARSKI:def_4;
hence  x in Y by A2, A3; ::_thesis: verum
end;
hence  for x being set holds
( x in Y iff for Z being set st Z in X holds
x in Z ) by A2; ::_thesis: verum
end;
thus  ( not X <> {} implies ex b1 being set st b1 = {} ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set holds
( ( X <> {} & ( for x being set holds
( x in b1 iff for Y being set st Y in X holds
x in Y ) ) & ( for x being set holds
( x in b2 iff for Y being set st Y in X holds
x in Y ) ) implies b1 = b2 ) & ( not X <> {} & b1 = {} & b2 = {} implies b1 = b2 ) )
proof
let Z1, Z2 be set ; ::_thesis: ( ( X <> {} & ( for x being set holds
( x in Z1 iff for Y being set st Y in X holds
x in Y ) ) & ( for x being set holds
( x in Z2 iff for Y being set st Y in X holds
x in Y ) ) implies Z1 = Z2 ) & ( not X <> {} & Z1 = {} & Z2 = {} implies Z1 = Z2 ) )
now__::_thesis:_(_X_<>_{}_&_(_for_x_being_set_holds_
(_x_in_Z1_iff_for_Y_being_set_st_Y_in_X_holds_
x_in_Y_)_)_&_(_for_x_being_set_holds_
(_x_in_Z2_iff_for_Y_being_set_st_Y_in_X_holds_
x_in_Y_)_)_implies_Z1_=_Z2_)
assume that
 X <> {} and
A4: for x being set holds
( x in Z1 iff for Y being set st Y in X holds
x in Y ) and
A5: for x being set holds
( x in Z2 iff for Y being set st Y in X holds
x in Y ) ; ::_thesis: Z1 = Z2
now__::_thesis:_for_x_being_set_holds_
(_x_in_Z1_iff_x_in_Z2_)
let x be set ; ::_thesis: ( x in Z1 iff x in Z2 )
 ( x in Z1 iff for Y being set st Y in X holds
x in Y ) by A4;
hence  ( x in Z1 iff x in Z2 ) by A5; ::_thesis: verum
end;
hence  Z1 = Z2 by TARSKI:1; ::_thesis: verum
end;
hence  ( ( X <> {} & ( for x being set holds
( x in Z1 iff for Y being set st Y in X holds
x in Y ) ) & ( for x being set holds
( x in Z2 iff for Y being set st Y in X holds
x in Y ) ) implies Z1 = Z2 ) & ( not X <> {} & Z1 = {} & Z2 = {} implies Z1 = Z2 ) ) ; ::_thesis: verum
end;
consistency
 for b1 being set holds verum ;
end;

:: deftheorem Def1 defines meet SETFAM_1:def_1_:_
 for X being set
for b2 being set holds
( ( X <> {} implies ( b2 = meet X iff for x being set holds
( x in b2 iff for Y being set st Y in X holds
x in Y ) ) ) & ( not X <> {} implies ( b2 = meet X iff b2 = {} ) ) );

theorem :: SETFAM_1:1
meet {} = {} by Def1;

theorem Th2: :: SETFAM_1:2
for X being set holds meet X c= union X
proof
let X be set ; ::_thesis: meet X c= union X
A1: now__::_thesis:_(_X_<>_{}_implies_meet_X_c=_union_X_)
assume A2: X <> {} ; ::_thesis: meet X c= union X
now__::_thesis:_for_x_being_set_st_x_in_meet_X_holds_
x_in_union_X
set y = the Element of X;
let x be set ; ::_thesis: ( x in meet X implies x in union X )
assume  x in meet X ; ::_thesis: x in union X
then  x in the Element of X by A2, Def1;
hence  x in union X by A2, TARSKI:def_4; ::_thesis: verum
end;
hence  meet X c= union X by TARSKI:def_3; ::_thesis: verum
end;
now__::_thesis:_(_X_=_{}_implies_meet_X_c=_union_X_)
assume  X = {} ; ::_thesis: meet X c= union X
then  meet X = {} by Def1;
hence  meet X c= union X by XBOOLE_1:2; ::_thesis: verum
end;
hence  meet X c= union X by A1; ::_thesis: verum
end;

theorem Th3: :: SETFAM_1:3
for Z, X being set st Z in X holds
meet X c= Z
proof
let Z, X be set ; ::_thesis: ( Z in X implies meet X c= Z )
assume A1: Z in X ; ::_thesis: meet X c= Z
 meet X c= Z
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet X or x in Z )
assume  x in meet X ; ::_thesis: x in Z
hence  x in Z by A1, Def1; ::_thesis: verum
end;
hence  meet X c= Z ; ::_thesis: verum
end;

theorem :: SETFAM_1:4
for X being set st {} in X holds
meet X = {} by Th3, XBOOLE_1:3;

theorem :: SETFAM_1:5
for X, Z being set st X <> {} & ( for Z1 being set st Z1 in X holds
Z c= Z1 ) holds
Z c= meet X
proof
let X, Z be set ; ::_thesis: ( X <> {} & ( for Z1 being set st Z1 in X holds
Z c= Z1 ) implies Z c= meet X )
assume that
A1: X <> {} and
A2: for Z1 being set st Z1 in X holds
Z c= Z1 ; ::_thesis: Z c= meet X
thus  Z c= meet X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in meet X )
assume A3: x in Z ; ::_thesis: x in meet X
 for Y being set st Y in X holds
x in Y
proof
let Y be set ; ::_thesis: ( Y in X implies x in Y )
assume  Y in X ; ::_thesis: x in Y
then  Z c= Y by A2;
hence  x in Y by A3; ::_thesis: verum
end;
hence  x in meet X by A1, Def1; ::_thesis: verum
end;
end;

theorem Th6: :: SETFAM_1:6
for X, Y being set st X <> {} & X c= Y holds
meet Y c= meet X
proof
let X, Y be set ; ::_thesis: ( X <> {} & X c= Y implies meet Y c= meet X )
assume that
A1: X <> {} and
A2: X c= Y ; ::_thesis: meet Y c= meet X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet Y or x in meet X )
assume  x in meet Y ; ::_thesis: x in meet X
then  for Z being set st Z in X holds
x in Z by A2, Def1;
hence  x in meet X by A1, Def1; ::_thesis: verum
end;

theorem :: SETFAM_1:7
for X, Y, Z being set st X in Y & X c= Z holds
meet Y c= Z
proof
let X, Y, Z be set ; ::_thesis: ( X in Y & X c= Z implies meet Y c= Z )
assume that
A1: X in Y and
A2: X c= Z ; ::_thesis: meet Y c= Z
 meet Y c= X by A1, Th3;
hence  meet Y c= Z by A2, XBOOLE_1:1; ::_thesis: verum
end;

theorem :: SETFAM_1:8
for X, Y, Z being set st X in Y & X misses Z holds
meet Y misses Z by Th3, XBOOLE_1:63;

theorem :: SETFAM_1:9
for X, Y being set st X <> {} & Y <> {} holds
meet (X \/ Y) = (meet X) /\ (meet Y)
proof
let X, Y be set ; ::_thesis: ( X <> {} & Y <> {} implies meet (X \/ Y) = (meet X) /\ (meet Y) )
assume that
A1: X <> {} and
A2: Y <> {} ; ::_thesis: meet (X \/ Y) = (meet X) /\ (meet Y)
A3: (meet X) /\ (meet Y) c= meet (X \/ Y)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (meet X) /\ (meet Y) or x in meet (X \/ Y) )
assume  x in (meet X) /\ (meet Y) ; ::_thesis: x in meet (X \/ Y)
then A4: ( x in meet X & x in meet Y ) by XBOOLE_0:def_4;
now__::_thesis:_for_Z_being_set_st_Z_in_X_\/_Y_holds_
x_in_Z
let Z be set ; ::_thesis: ( Z in X \/ Y implies x in Z )
assume  Z in X \/ Y ; ::_thesis: x in Z
then  ( Z in X or Z in Y ) by XBOOLE_0:def_3;
hence  x in Z by A4, Def1; ::_thesis: verum
end;
hence  x in meet (X \/ Y) by A1, Def1; ::_thesis: verum
end;
 ( meet (X \/ Y) c= meet X & meet (X \/ Y) c= meet Y ) by A1, A2, Th6, XBOOLE_1:7;
then  meet (X \/ Y) c= (meet X) /\ (meet Y) by XBOOLE_1:19;
hence  meet (X \/ Y) = (meet X) /\ (meet Y) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: SETFAM_1:10
for x being set holds meet {x} = x
proof
let x be set ; ::_thesis: meet {x} = x
A1: x c= meet {x}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x or y in meet {x} )
assume  y in x ; ::_thesis: y in meet {x}
then  for Z being set st Z in {x} holds
y in Z by TARSKI:def_1;
hence  y in meet {x} by Def1; ::_thesis: verum
end;
 x in {x} by TARSKI:def_1;
then  meet {x} c= x by Th3;
hence  meet {x} = x by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: SETFAM_1:11
for X, Y being set holds meet {X,Y} = X /\ Y
proof
let X, Y be set ; ::_thesis: meet {X,Y} = X /\ Y
A1: ( X in {X,Y} & Y in {X,Y} ) by TARSKI:def_2;
 for x being set holds
( x in meet {X,Y} iff ( x in X & x in Y ) )
proof
let x be set ; ::_thesis: ( x in meet {X,Y} iff ( x in X & x in Y ) )
thus  ( x in meet {X,Y} implies ( x in X & x in Y ) ) by A1, Def1; ::_thesis: ( x in X & x in Y implies x in meet {X,Y} )
assume  ( x in X & x in Y ) ; ::_thesis: x in meet {X,Y}
then  for Z being set st Z in {X,Y} holds
x in Z by TARSKI:def_2;
hence  x in meet {X,Y} by Def1; ::_thesis: verum
end;
hence  meet {X,Y} = X /\ Y by XBOOLE_0:def_4; ::_thesis: verum
end;


definition
let SFX, SFY be set ;
predSFX is_finer_than SFY means :: SETFAM_1:def 2
 for X being set st X in SFX holds
ex Y being set st
( Y in SFY & X c= Y );
reflexivity
 for SFX, X being set st X in SFX holds
ex Y being set st
( Y in SFX & X c= Y ) ;
predSFY is_coarser_than SFX means :: SETFAM_1:def 3
 for Y being set st Y in SFY holds
ex X being set st
( X in SFX & X c= Y );
reflexivity
 for SFY, Y being set st Y in SFY holds
ex X being set st
( X in SFY & X c= Y ) ;
end;

:: deftheorem  defines is_finer_than SETFAM_1:def_2_:_
 for SFX, SFY being set holds
( SFX is_finer_than SFY iff for X being set st X in SFX holds
ex Y being set st
( Y in SFY & X c= Y ) );

:: deftheorem  defines is_coarser_than SETFAM_1:def_3_:_
 for SFX, SFY being set holds
( SFY is_coarser_than SFX iff for Y being set st Y in SFY holds
ex X being set st
( X in SFX & X c= Y ) );

theorem :: SETFAM_1:12
for SFX, SFY being set st SFX c= SFY holds
SFX is_finer_than SFY
proof
let SFX, SFY be set ; ::_thesis: ( SFX c= SFY implies SFX is_finer_than SFY )
assume A1: SFX c= SFY ; ::_thesis: SFX is_finer_than SFY
let X be set ; :: according to SETFAM_1:def_2 ::_thesis: ( X in SFX implies ex Y being set st
( Y in SFY & X c= Y ) )
assume A2: X in SFX ; ::_thesis: ex Y being set st
( Y in SFY & X c= Y )
take  X ; ::_thesis: ( X in SFY & X c= X )
thus  ( X in SFY & X c= X ) by A1, A2; ::_thesis: verum
end;

theorem :: SETFAM_1:13
for SFX, SFY being set st SFX is_finer_than SFY holds
union SFX c= union SFY
proof
let SFX, SFY be set ; ::_thesis: ( SFX is_finer_than SFY implies union SFX c= union SFY )
assume A1: for X being set st X in SFX holds
ex Y being set st
( Y in SFY & X c= Y ) ; :: according to SETFAM_1:def_2 ::_thesis: union SFX c= union SFY
thus  union SFX c= union SFY ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union SFX or x in union SFY )
assume  x in union SFX ; ::_thesis: x in union SFY
then consider Y being set  such that
A2: x in Y and
A3: Y in SFX by TARSKI:def_4;
 ex Z being set st
( Z in SFY & Y c= Z ) by A1, A3;
hence  x in union SFY by A2, TARSKI:def_4; ::_thesis: verum
end;
end;

theorem :: SETFAM_1:14
for SFY, SFX being set st SFY <> {} & SFY is_coarser_than SFX holds
meet SFX c= meet SFY
proof
let SFY, SFX be set ; ::_thesis: ( SFY <> {} & SFY is_coarser_than SFX implies meet SFX c= meet SFY )
assume that
A1: SFY <> {} and
A2: for Z2 being set st Z2 in SFY holds
ex Z1 being set st
( Z1 in SFX & Z1 c= Z2 ) ; :: according to SETFAM_1:def_3 ::_thesis: meet SFX c= meet SFY
 meet SFX c= meet SFY
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet SFX or x in meet SFY )
assume A3: x in meet SFX ; ::_thesis: x in meet SFY
 for Z being set st Z in SFY holds
x in Z
proof
let Z be set ; ::_thesis: ( Z in SFY implies x in Z )
assume  Z in SFY ; ::_thesis: x in Z
then consider Z1 being set  such that
A4: Z1 in SFX and
A5: Z1 c= Z by A2;
 x in Z1 by A3, A4, Def1;
hence  x in Z by A5; ::_thesis: verum
end;
hence  x in meet SFY by A1, Def1; ::_thesis: verum
end;
hence  meet SFX c= meet SFY ; ::_thesis: verum
end;

theorem :: SETFAM_1:15
for SFX being set holds {} is_finer_than SFX
proof
let SFX be set ; ::_thesis: {} is_finer_than SFX
let X be set ; :: according to SETFAM_1:def_2 ::_thesis: ( X in {} implies ex Y being set st
( Y in SFX & X c= Y ) )
assume  X in {} ; ::_thesis: ex Y being set st
( Y in SFX & X c= Y )
hence  ex Y being set st
( Y in SFX & X c= Y ) ; ::_thesis: verum
end;

theorem :: SETFAM_1:16
for SFX being set st SFX is_finer_than {} holds
SFX = {}
proof
let SFX be set ; ::_thesis: ( SFX is_finer_than {} implies SFX = {} )
assume A1: for X being set st X in SFX holds
ex Y being set st
( Y in {} & X c= Y ) ; :: according to SETFAM_1:def_2 ::_thesis: SFX = {}
set x = the Element of SFX;
assume  not SFX = {} ; ::_thesis: contradiction
then  ex Y being set st
( Y in {} & the Element of SFX c= Y ) by A1;
hence  contradiction ; ::_thesis: verum
end;

theorem :: SETFAM_1:17
for SFX, SFY, SFZ being set st SFX is_finer_than SFY & SFY is_finer_than SFZ holds
SFX is_finer_than SFZ
proof
let SFX, SFY, SFZ be set ; ::_thesis: ( SFX is_finer_than SFY & SFY is_finer_than SFZ implies SFX is_finer_than SFZ )
assume that
A1: for X being set st X in SFX holds
ex Y being set st
( Y in SFY & X c= Y ) and
A2: for X being set st X in SFY holds
ex Y being set st
( Y in SFZ & X c= Y ) ; :: according to SETFAM_1:def_2 ::_thesis: SFX is_finer_than SFZ
let X be set ; :: according to SETFAM_1:def_2 ::_thesis: ( X in SFX implies ex Y being set st
( Y in SFZ & X c= Y ) )
assume  X in SFX ; ::_thesis: ex Y being set st
( Y in SFZ & X c= Y )
then consider Y being set  such that
A3: Y in SFY and
A4: X c= Y by A1;
consider Z being set  such that
A5: ( Z in SFZ & Y c= Z ) by A2, A3;
take  Z ; ::_thesis: ( Z in SFZ & X c= Z )
thus  ( Z in SFZ & X c= Z ) by A4, A5, XBOOLE_1:1; ::_thesis: verum
end;

theorem :: SETFAM_1:18
for Y, SFX being set st SFX is_finer_than {Y} holds
for X being set st X in SFX holds
X c= Y
proof
let Y, SFX be set ; ::_thesis: ( SFX is_finer_than {Y} implies for X being set st X in SFX holds
X c= Y )
assume A1: for X being set st X in SFX holds
ex Z being set st
( Z in {Y} & X c= Z ) ; :: according to SETFAM_1:def_2 ::_thesis: for X being set st X in SFX holds
X c= Y
let X be set ; ::_thesis: ( X in SFX implies X c= Y )
assume  X in SFX ; ::_thesis: X c= Y
then  ex Z being set st
( Z in {Y} & X c= Z ) by A1;
hence  X c= Y by TARSKI:def_1; ::_thesis: verum
end;

theorem :: SETFAM_1:19
for X, Y, SFX being set st SFX is_finer_than {X,Y} holds
for Z being set holds
( not Z in SFX or Z c= X or Z c= Y )
proof
let X, Y, SFX be set ; ::_thesis: ( SFX is_finer_than {X,Y} implies for Z being set holds
( not Z in SFX or Z c= X or Z c= Y ) )
assume A1: for Z1 being set st Z1 in SFX holds
ex Z2 being set st
( Z2 in {X,Y} & Z1 c= Z2 ) ; :: according to SETFAM_1:def_2 ::_thesis: for Z being set holds
( not Z in SFX or Z c= X or Z c= Y )
let Z be set ; ::_thesis: ( not Z in SFX or Z c= X or Z c= Y )
assume  Z in SFX ; ::_thesis: ( Z c= X or Z c= Y )
then consider Z2 being set  such that
A2: Z2 in {X,Y} and
A3: Z c= Z2 by A1;
 {X,Y} = {X} \/ {Y} by ENUMSET1:1;
then  ( Z2 in {X} or Z2 in {Y} ) by A2, XBOOLE_0:def_3;
hence  ( Z c= X or Z c= Y ) by A3, TARSKI:def_1; ::_thesis: verum
end;

definition
let SFX, SFY be set ;
func UNION (SFX,SFY) ->  set  means :Def4: :: SETFAM_1:def 4
 for Z being set holds
( Z in it iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) );
existence
 ex b1 being set st
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) )
proof
defpred S1[ set ] means  ex Z being set st
( $1 = Z & ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) );
consider XX being set  such that
A1: for x being set holds
( x in XX iff ( x in bool ((union SFX) \/ (union SFY)) & S1[x] ) ) from XBOOLE_0:sch_1();
take  XX ; ::_thesis: for Z being set holds
( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) )
 for Z being set holds
( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) )
proof
let Z be set ; ::_thesis: ( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) )
A2: now__::_thesis:_(_ex_X,_Y_being_set_st_
(_X_in_SFX_&_Y_in_SFY_&_Z_=_X_\/_Y_)_implies_Z_in_XX_)
given X, Y being set  such that A3: ( X in SFX & Y in SFY ) and
A4: Z = X \/ Y ; ::_thesis: Z in XX
 ( X c= union SFX & Y c= union SFY ) by A3, ZFMISC_1:74;
then  Z c= (union SFX) \/ (union SFY) by A4, XBOOLE_1:13;
hence  Z in XX by A1, A3, A4; ::_thesis: verum
end;
now__::_thesis:_(_Z_in_XX_implies_ex_X,_Y_being_set_st_
(_X_in_SFX_&_Y_in_SFY_&_Z_=_X_\/_Y_)_)
assume  Z in XX ; ::_thesis: ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y )
then  ex Z1 being set st
( Z = Z1 & ex X, Y being set st
( X in SFX & Y in SFY & Z1 = X \/ Y ) ) by A1;
hence  ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ; ::_thesis: verum
end;
hence  ( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) by A2; ::_thesis: verum
end;
hence  for Z being set holds
( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) & ( for Z being set holds
( Z in b2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) holds
b1 = b2
proof
let Z1, Z2 be set ; ::_thesis: ( ( for Z being set holds
( Z in Z1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) & ( for Z being set holds
( Z in Z2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) implies Z1 = Z2 )
assume that
A5: for Z being set holds
( Z in Z1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) and
A6: for Z being set holds
( Z in Z2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ; ::_thesis: Z1 = Z2
now__::_thesis:_for_Z_being_set_holds_
(_Z_in_Z1_iff_Z_in_Z2_)
let Z be set ; ::_thesis: ( Z in Z1 iff Z in Z2 )
 ( Z in Z1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) by A5;
hence  ( Z in Z1 iff Z in Z2 ) by A6; ::_thesis: verum
end;
hence  Z1 = Z2 by TARSKI:1; ::_thesis: verum
end;
commutativity
 for b1 being set
for SFX, SFY being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) holds
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X \/ Y ) )
proof
let SFZ, SFX, SFY be set ; ::_thesis: ( ( for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ) implies for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X \/ Y ) ) )
assume A7: for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) ; ::_thesis: for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X \/ Y ) )
let Z be set ; ::_thesis: ( Z in SFZ iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X \/ Y ) )
hereby  ::_thesis: ( ex X, Y being set st
( X in SFY & Y in SFX & Z = X \/ Y ) implies Z in SFZ )
assume  Z in SFZ ; ::_thesis: ex Y, X being set st
( Y in SFY & X in SFX & Z = Y \/ X )
then  ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) by A7;
hence  ex Y, X being set st
( Y in SFY & X in SFX & Z = Y \/ X ) ; ::_thesis: verum
end;
thus  ( ex X, Y being set st
( X in SFY & Y in SFX & Z = X \/ Y ) implies Z in SFZ ) by A7; ::_thesis: verum
end;
func INTERSECTION (SFX,SFY) ->  set  means :Def5: :: SETFAM_1:def 5
 for Z being set holds
( Z in it iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) );
existence
 ex b1 being set st
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) )
proof
defpred S1[ set ] means  ex Z being set st
( $1 = Z & ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) );
consider XX being set  such that
A8: for x being set holds
( x in XX iff ( x in bool ((union SFX) /\ (union SFY)) & S1[x] ) ) from XBOOLE_0:sch_1();
take  XX ; ::_thesis: for Z being set holds
( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) )
 for Z being set holds
( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) )
proof
let Z be set ; ::_thesis: ( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) )
A9: now__::_thesis:_(_ex_X,_Y_being_set_st_
(_X_in_SFX_&_Y_in_SFY_&_Z_=_X_/\_Y_)_implies_Z_in_XX_)
given X, Y being set  such that A10: ( X in SFX & Y in SFY ) and
A11: Z = X /\ Y ; ::_thesis: Z in XX
 ( X c= union SFX & Y c= union SFY ) by A10, ZFMISC_1:74;
then  Z c= (union SFX) /\ (union SFY) by A11, XBOOLE_1:27;
hence  Z in XX by A8, A10, A11; ::_thesis: verum
end;
now__::_thesis:_(_Z_in_XX_implies_ex_X,_Y_being_set_st_
(_X_in_SFX_&_Y_in_SFY_&_Z_=_X_/\_Y_)_)
assume  Z in XX ; ::_thesis: ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y )
then  ex Z1 being set st
( Z = Z1 & ex X, Y being set st
( X in SFX & Y in SFY & Z1 = X /\ Y ) ) by A8;
hence  ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ; ::_thesis: verum
end;
hence  ( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) by A9; ::_thesis: verum
end;
hence  for Z being set holds
( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) & ( for Z being set holds
( Z in b2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) holds
b1 = b2
proof
let Z1, Z2 be set ; ::_thesis: ( ( for Z being set holds
( Z in Z1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) & ( for Z being set holds
( Z in Z2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) implies Z1 = Z2 )
assume that
A12: for Z being set holds
( Z in Z1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) and
A13: for Z being set holds
( Z in Z2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ; ::_thesis: Z1 = Z2
now__::_thesis:_for_Z_being_set_holds_
(_Z_in_Z1_iff_Z_in_Z2_)
let Z be set ; ::_thesis: ( Z in Z1 iff Z in Z2 )
 ( Z in Z1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) by A12;
hence  ( Z in Z1 iff Z in Z2 ) by A13; ::_thesis: verum
end;
hence  Z1 = Z2 by TARSKI:1; ::_thesis: verum
end;
commutativity
 for b1 being set
for SFX, SFY being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) holds
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) )
proof
let SFZ, SFX, SFY be set ; ::_thesis: ( ( for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ) implies for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) ) )
assume A14: for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) ; ::_thesis: for Z being set holds
( Z in SFZ iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) )
let Z be set ; ::_thesis: ( Z in SFZ iff ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) )
hereby  ::_thesis: ( ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) implies Z in SFZ )
assume  Z in SFZ ; ::_thesis: ex Y, X being set st
( Y in SFY & X in SFX & Z = Y /\ X )
then  ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) by A14;
hence  ex Y, X being set st
( Y in SFY & X in SFX & Z = Y /\ X ) ; ::_thesis: verum
end;
thus  ( ex X, Y being set st
( X in SFY & Y in SFX & Z = X /\ Y ) implies Z in SFZ ) by A14; ::_thesis: verum
end;
func DIFFERENCE (SFX,SFY) ->  set  means :Def6: :: SETFAM_1:def 6
 for Z being set holds
( Z in it iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) );
existence
 ex b1 being set st
for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) )
proof
defpred S1[ set ] means  ex Z being set st
( $1 = Z & ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) );
consider XX being set  such that
A15: for x being set holds
( x in XX iff ( x in bool (union SFX) & S1[x] ) ) from XBOOLE_0:sch_1();
take  XX ; ::_thesis: for Z being set holds
( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) )
 for Z being set holds
( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) )
proof
let Z be set ; ::_thesis: ( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) )
A16: now__::_thesis:_(_ex_X,_Y_being_set_st_
(_X_in_SFX_&_Y_in_SFY_&_Z_=_X_\_Y_)_implies_Z_in_XX_)
given X, Y being set  such that A17: X in SFX and
A18: Y in SFY and
A19: Z = X \ Y ; ::_thesis: Z in XX
 X c= union SFX by A17, ZFMISC_1:74;
then  Z c= union SFX by A19, XBOOLE_1:1;
hence  Z in XX by A15, A17, A18, A19; ::_thesis: verum
end;
now__::_thesis:_(_Z_in_XX_implies_ex_X,_Y_being_set_st_
(_X_in_SFX_&_Y_in_SFY_&_Z_=_X_\_Y_)_)
assume  Z in XX ; ::_thesis: ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y )
then  ex Z1 being set st
( Z = Z1 & ex X, Y being set st
( X in SFX & Y in SFY & Z1 = X \ Y ) ) by A15;
hence  ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ; ::_thesis: verum
end;
hence  ( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) by A16; ::_thesis: verum
end;
hence  for Z being set holds
( Z in XX iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for Z being set holds
( Z in b1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) ) & ( for Z being set holds
( Z in b2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) ) holds
b1 = b2
proof
let Z1, Z2 be set ; ::_thesis: ( ( for Z being set holds
( Z in Z1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) ) & ( for Z being set holds
( Z in Z2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) ) implies Z1 = Z2 )
assume that
A20: for Z being set holds
( Z in Z1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) and
A21: for Z being set holds
( Z in Z2 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) ; ::_thesis: Z1 = Z2
now__::_thesis:_for_Z_being_set_holds_
(_Z_in_Z1_iff_Z_in_Z2_)
let Z be set ; ::_thesis: ( Z in Z1 iff Z in Z2 )
 ( Z in Z1 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) by A20;
hence  ( Z in Z1 iff Z in Z2 ) by A21; ::_thesis: verum
end;
hence  Z1 = Z2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines UNION SETFAM_1:def_4_:_
 for SFX, SFY being set
for b3 being set holds
( b3 = UNION (SFX,SFY) iff for Z being set holds
( Z in b3 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \/ Y ) ) );

:: deftheorem Def5 defines INTERSECTION SETFAM_1:def_5_:_
 for SFX, SFY being set
for b3 being set holds
( b3 = INTERSECTION (SFX,SFY) iff for Z being set holds
( Z in b3 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X /\ Y ) ) );

:: deftheorem Def6 defines DIFFERENCE SETFAM_1:def_6_:_
 for SFX, SFY being set
for b3 being set holds
( b3 = DIFFERENCE (SFX,SFY) iff for Z being set holds
( Z in b3 iff ex X, Y being set st
( X in SFX & Y in SFY & Z = X \ Y ) ) );

theorem :: SETFAM_1:20
for SFX being set holds SFX is_finer_than UNION (SFX,SFX)
proof
let SFX be set ; ::_thesis: SFX is_finer_than UNION (SFX,SFX)
let X be set ; :: according to SETFAM_1:def_2 ::_thesis: ( X in SFX implies ex Y being set st
( Y in UNION (SFX,SFX) & X c= Y ) )
assume A1: X in SFX ; ::_thesis: ex Y being set st
( Y in UNION (SFX,SFX) & X c= Y )
take  X ; ::_thesis: ( X in UNION (SFX,SFX) & X c= X )
 X = X \/ X ;
hence  ( X in UNION (SFX,SFX) & X c= X ) by A1, Def4; ::_thesis: verum
end;

theorem :: SETFAM_1:21
for SFX being set holds INTERSECTION (SFX,SFX) is_finer_than SFX
proof
let SFX be set ; ::_thesis: INTERSECTION (SFX,SFX) is_finer_than SFX
let X be set ; :: according to SETFAM_1:def_2 ::_thesis: ( X in INTERSECTION (SFX,SFX) implies ex Y being set st
( Y in SFX & X c= Y ) )
assume  X in INTERSECTION (SFX,SFX) ; ::_thesis: ex Y being set st
( Y in SFX & X c= Y )
then consider Z1, Z2 being set  such that
A1: Z1 in SFX and
 Z2 in SFX and
A2: X = Z1 /\ Z2 by Def5;
take  Z1 ; ::_thesis: ( Z1 in SFX & X c= Z1 )
thus  ( Z1 in SFX & X c= Z1 ) by A1, A2, XBOOLE_1:17; ::_thesis: verum
end;

theorem :: SETFAM_1:22
for SFX being set holds DIFFERENCE (SFX,SFX) is_finer_than SFX
proof
let SFX be set ; ::_thesis: DIFFERENCE (SFX,SFX) is_finer_than SFX
let X be set ; :: according to SETFAM_1:def_2 ::_thesis: ( X in DIFFERENCE (SFX,SFX) implies ex Y being set st
( Y in SFX & X c= Y ) )
assume  X in DIFFERENCE (SFX,SFX) ; ::_thesis: ex Y being set st
( Y in SFX & X c= Y )
then consider Z1, Z2 being set  such that
A1: Z1 in SFX and
 Z2 in SFX and
A2: X = Z1 \ Z2 by Def6;
take  Z1 ; ::_thesis: ( Z1 in SFX & X c= Z1 )
thus  ( Z1 in SFX & X c= Z1 ) by A1, A2; ::_thesis: verum
end;

theorem :: SETFAM_1:23
for SFX, SFY being set st SFX meets SFY holds
(meet SFX) /\ (meet SFY) = meet (INTERSECTION (SFX,SFY))
proof
let SFX, SFY be set ; ::_thesis: ( SFX meets SFY implies (meet SFX) /\ (meet SFY) = meet (INTERSECTION (SFX,SFY)) )
set y = the Element of SFX /\ SFY;
assume A1: SFX /\ SFY <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: (meet SFX) /\ (meet SFY) = meet (INTERSECTION (SFX,SFY))
then A2: SFY <> {} ;
A3: the Element of SFX /\ SFY in SFX by A1, XBOOLE_0:def_4;
A4: the Element of SFX /\ SFY in SFY by A1, XBOOLE_0:def_4;
A5: SFX <> {} by A1;
A6: meet (INTERSECTION (SFX,SFY)) c= (meet SFX) /\ (meet SFY)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (INTERSECTION (SFX,SFY)) or x in (meet SFX) /\ (meet SFY) )
assume A7: x in meet (INTERSECTION (SFX,SFY)) ; ::_thesis: x in (meet SFX) /\ (meet SFY)
 for Z being set st Z in SFY holds
x in Z
proof
let Z be set ; ::_thesis: ( Z in SFY implies x in Z )
assume  Z in SFY ; ::_thesis: x in Z
then  the Element of SFX /\ SFY /\ Z in INTERSECTION (SFX,SFY) by A3, Def5;
then  x in the Element of SFX /\ SFY /\ Z by A7, Def1;
hence  x in Z by XBOOLE_0:def_4; ::_thesis: verum
end;
then A8: x in meet SFY by A2, Def1;
 for Z being set st Z in SFX holds
x in Z
proof
let Z be set ; ::_thesis: ( Z in SFX implies x in Z )
assume  Z in SFX ; ::_thesis: x in Z
then  Z /\ the Element of SFX /\ SFY in INTERSECTION (SFX,SFY) by A4, Def5;
then  x in Z /\ the Element of SFX /\ SFY by A7, Def1;
hence  x in Z by XBOOLE_0:def_4; ::_thesis: verum
end;
then  x in meet SFX by A5, Def1;
hence  x in (meet SFX) /\ (meet SFY) by A8, XBOOLE_0:def_4; ::_thesis: verum
end;
A9: the Element of SFX /\ SFY /\ the Element of SFX /\ SFY in INTERSECTION (SFX,SFY) by A3, A4, Def5;
 (meet SFX) /\ (meet SFY) c= meet (INTERSECTION (SFX,SFY))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (meet SFX) /\ (meet SFY) or x in meet (INTERSECTION (SFX,SFY)) )
assume  x in (meet SFX) /\ (meet SFY) ; ::_thesis: x in meet (INTERSECTION (SFX,SFY))
then A10: ( x in meet SFX & x in meet SFY ) by XBOOLE_0:def_4;
 for Z being set st Z in INTERSECTION (SFX,SFY) holds
x in Z
proof
let Z be set ; ::_thesis: ( Z in INTERSECTION (SFX,SFY) implies x in Z )
assume  Z in INTERSECTION (SFX,SFY) ; ::_thesis: x in Z
then consider Z1, Z2 being set  such that
A11: ( Z1 in SFX & Z2 in SFY ) and
A12: Z = Z1 /\ Z2 by Def5;
 ( x in Z1 & x in Z2 ) by A10, A11, Def1;
hence  x in Z by A12, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  x in meet (INTERSECTION (SFX,SFY)) by A9, Def1; ::_thesis: verum
end;
hence  (meet SFX) /\ (meet SFY) = meet (INTERSECTION (SFX,SFY)) by A6, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: SETFAM_1:24
for X, SFY being set st SFY <> {} holds
X \/ (meet SFY) = meet (UNION ({X},SFY))
proof
let X, SFY be set ; ::_thesis: ( SFY <> {} implies X \/ (meet SFY) = meet (UNION ({X},SFY)) )
assume A1: SFY <> {} ; ::_thesis: X \/ (meet SFY) = meet (UNION ({X},SFY))
set y = the Element of SFY;
 X in {X} by TARSKI:def_1;
then A2: X \/ the Element of SFY in UNION ({X},SFY) by A1, Def4;
A3: X \/ (meet SFY) c= meet (UNION ({X},SFY))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \/ (meet SFY) or x in meet (UNION ({X},SFY)) )
assume  x in X \/ (meet SFY) ; ::_thesis: x in meet (UNION ({X},SFY))
then A4: ( x in X or x in meet SFY ) by XBOOLE_0:def_3;
 for Z being set st Z in UNION ({X},SFY) holds
x in Z
proof
let Z be set ; ::_thesis: ( Z in UNION ({X},SFY) implies x in Z )
assume  Z in UNION ({X},SFY) ; ::_thesis: x in Z
then consider Z1, Z2 being set  such that
A5: ( Z1 in {X} & Z2 in SFY ) and
A6: Z = Z1 \/ Z2 by Def4;
 ( x in Z1 or x in Z2 ) by A4, A5, Def1, TARSKI:def_1;
hence  x in Z by A6, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  x in meet (UNION ({X},SFY)) by A2, Def1; ::_thesis: verum
end;
 meet (UNION ({X},SFY)) c= X \/ (meet SFY)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (UNION ({X},SFY)) or x in X \/ (meet SFY) )
assume A7: x in meet (UNION ({X},SFY)) ; ::_thesis: x in X \/ (meet SFY)
assume A8: not x in X \/ (meet SFY) ; ::_thesis: contradiction
then A9: not x in X by XBOOLE_0:def_3;
 not x in meet SFY by A8, XBOOLE_0:def_3;
then consider Z being set  such that
A10: Z in SFY and
A11: not x in Z by A1, Def1;
 X in {X} by TARSKI:def_1;
then  X \/ Z in UNION ({X},SFY) by A10, Def4;
then  x in X \/ Z by A7, Def1;
hence  contradiction by A9, A11, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  X \/ (meet SFY) = meet (UNION ({X},SFY)) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: SETFAM_1:25
for X, SFY being set holds X /\ (union SFY) = union (INTERSECTION ({X},SFY))
proof
let X, SFY be set ; ::_thesis: X /\ (union SFY) = union (INTERSECTION ({X},SFY))
A1: union (INTERSECTION ({X},SFY)) c= X /\ (union SFY)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (INTERSECTION ({X},SFY)) or x in X /\ (union SFY) )
assume  x in union (INTERSECTION ({X},SFY)) ; ::_thesis: x in X /\ (union SFY)
then consider Z being set  such that
A2: x in Z and
A3: Z in INTERSECTION ({X},SFY) by TARSKI:def_4;
consider X1, X2 being set  such that
A4: X1 in {X} and
A5: X2 in SFY and
A6: Z = X1 /\ X2 by A3, Def5;
 x in X2 by A2, A6, XBOOLE_0:def_4;
then A7: x in union SFY by A5, TARSKI:def_4;
 X1 = X by A4, TARSKI:def_1;
then  x in X by A2, A6, XBOOLE_0:def_4;
hence  x in X /\ (union SFY) by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
 X /\ (union SFY) c= union (INTERSECTION ({X},SFY))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X /\ (union SFY) or x in union (INTERSECTION ({X},SFY)) )
assume A8: x in X /\ (union SFY) ; ::_thesis: x in union (INTERSECTION ({X},SFY))
then  x in union SFY by XBOOLE_0:def_4;
then consider Y being set  such that
A9: x in Y and
A10: Y in SFY by TARSKI:def_4;
 x in X by A8, XBOOLE_0:def_4;
then A11: x in X /\ Y by A9, XBOOLE_0:def_4;
 X in {X} by TARSKI:def_1;
then  X /\ Y in INTERSECTION ({X},SFY) by A10, Def5;
hence  x in union (INTERSECTION ({X},SFY)) by A11, TARSKI:def_4; ::_thesis: verum
end;
hence  X /\ (union SFY) = union (INTERSECTION ({X},SFY)) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: SETFAM_1:26
for X, SFY being set st SFY <> {} holds
X \ (union SFY) = meet (DIFFERENCE ({X},SFY))
proof
let X, SFY be set ; ::_thesis: ( SFY <> {} implies X \ (union SFY) = meet (DIFFERENCE ({X},SFY)) )
set y = the Element of SFY;
A1: X in {X} by TARSKI:def_1;
assume  SFY <> {} ; ::_thesis: X \ (union SFY) = meet (DIFFERENCE ({X},SFY))
then A2: X \ the Element of SFY in DIFFERENCE ({X},SFY) by A1, Def6;
A3: meet (DIFFERENCE ({X},SFY)) c= X \ (union SFY)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (DIFFERENCE ({X},SFY)) or x in X \ (union SFY) )
assume A4: x in meet (DIFFERENCE ({X},SFY)) ; ::_thesis: x in X \ (union SFY)
 for Z being set st Z in SFY holds
not x in Z
proof
let Z be set ; ::_thesis: ( Z in SFY implies not x in Z )
assume  Z in SFY ; ::_thesis: not x in Z
then  X \ Z in DIFFERENCE ({X},SFY) by A1, Def6;
then  x in X \ Z by A4, Def1;
hence  not x in Z by XBOOLE_0:def_5; ::_thesis: verum
end;
then  for Z being set st x in Z holds
not Z in SFY ;
then A5: not x in union SFY by TARSKI:def_4;
 x in X \ the Element of SFY by A2, A4, Def1;
hence  x in X \ (union SFY) by A5, XBOOLE_0:def_5; ::_thesis: verum
end;
 X \ (union SFY) c= meet (DIFFERENCE ({X},SFY))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \ (union SFY) or x in meet (DIFFERENCE ({X},SFY)) )
assume  x in X \ (union SFY) ; ::_thesis: x in meet (DIFFERENCE ({X},SFY))
then A6: ( x in X & not x in union SFY ) by XBOOLE_0:def_5;
 for Z being set st Z in DIFFERENCE ({X},SFY) holds
x in Z
proof
let Z be set ; ::_thesis: ( Z in DIFFERENCE ({X},SFY) implies x in Z )
assume  Z in DIFFERENCE ({X},SFY) ; ::_thesis: x in Z
then consider Z1, Z2 being set  such that
A7: ( Z1 in {X} & Z2 in SFY ) and
A8: Z = Z1 \ Z2 by Def6;
 ( x in Z1 & not x in Z2 ) by A6, A7, TARSKI:def_1, TARSKI:def_4;
hence  x in Z by A8, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  x in meet (DIFFERENCE ({X},SFY)) by A2, Def1; ::_thesis: verum
end;
hence  X \ (union SFY) = meet (DIFFERENCE ({X},SFY)) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: SETFAM_1:27
for X, SFY being set st SFY <> {} holds
X \ (meet SFY) = union (DIFFERENCE ({X},SFY))
proof
let X, SFY be set ; ::_thesis: ( SFY <> {} implies X \ (meet SFY) = union (DIFFERENCE ({X},SFY)) )
A1: X in {X} by TARSKI:def_1;
A2: union (DIFFERENCE ({X},SFY)) c= X \ (meet SFY)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (DIFFERENCE ({X},SFY)) or x in X \ (meet SFY) )
assume  x in union (DIFFERENCE ({X},SFY)) ; ::_thesis: x in X \ (meet SFY)
then consider Z being set  such that
A3: x in Z and
A4: Z in DIFFERENCE ({X},SFY) by TARSKI:def_4;
consider Z1, Z2 being set  such that
A5: Z1 in {X} and
A6: Z2 in SFY and
A7: Z = Z1 \ Z2 by A4, Def6;
 not x in Z2 by A3, A7, XBOOLE_0:def_5;
then A8: not x in meet SFY by A6, Def1;
 Z1 = X by A5, TARSKI:def_1;
hence  x in X \ (meet SFY) by A3, A7, A8, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A9: SFY <> {} ; ::_thesis: X \ (meet SFY) = union (DIFFERENCE ({X},SFY))
 X \ (meet SFY) c= union (DIFFERENCE ({X},SFY))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \ (meet SFY) or x in union (DIFFERENCE ({X},SFY)) )
assume A10: x in X \ (meet SFY) ; ::_thesis: x in union (DIFFERENCE ({X},SFY))
then  not x in meet SFY by XBOOLE_0:def_5;
then consider Z being set  such that
A11: Z in SFY and
A12: not x in Z by A9, Def1;
A13: x in X \ Z by A10, A12, XBOOLE_0:def_5;
 X \ Z in DIFFERENCE ({X},SFY) by A1, A11, Def6;
hence  x in union (DIFFERENCE ({X},SFY)) by A13, TARSKI:def_4; ::_thesis: verum
end;
hence  X \ (meet SFY) = union (DIFFERENCE ({X},SFY)) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: SETFAM_1:28
for SFX, SFY being set holds union (INTERSECTION (SFX,SFY)) = (union SFX) /\ (union SFY)
proof
let SFX, SFY be set ; ::_thesis: union (INTERSECTION (SFX,SFY)) = (union SFX) /\ (union SFY)
thus  union (INTERSECTION (SFX,SFY)) c= (union SFX) /\ (union SFY) :: according to XBOOLE_0:def_10 ::_thesis: (union SFX) /\ (union SFY) c= union (INTERSECTION (SFX,SFY))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (INTERSECTION (SFX,SFY)) or x in (union SFX) /\ (union SFY) )
assume  x in union (INTERSECTION (SFX,SFY)) ; ::_thesis: x in (union SFX) /\ (union SFY)
then consider Z being set  such that
A1: x in Z and
A2: Z in INTERSECTION (SFX,SFY) by TARSKI:def_4;
consider X, Y being set  such that
A3: X in SFX and
A4: Y in SFY and
A5: Z = X /\ Y by A2, Def5;
 x in Y by A1, A5, XBOOLE_0:def_4;
then A6: x in union SFY by A4, TARSKI:def_4;
 x in X by A1, A5, XBOOLE_0:def_4;
then  x in union SFX by A3, TARSKI:def_4;
hence  x in (union SFX) /\ (union SFY) by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (union SFX) /\ (union SFY) or x in union (INTERSECTION (SFX,SFY)) )
assume A7: x in (union SFX) /\ (union SFY) ; ::_thesis: x in union (INTERSECTION (SFX,SFY))
then  x in union SFX by XBOOLE_0:def_4;
then consider X0 being set  such that
A8: ( x in X0 & X0 in SFX ) by TARSKI:def_4;
 x in union SFY by A7, XBOOLE_0:def_4;
then consider Y0 being set  such that
A9: ( x in Y0 & Y0 in SFY ) by TARSKI:def_4;
 ( X0 /\ Y0 in INTERSECTION (SFX,SFY) & x in X0 /\ Y0 ) by A8, A9, Def5, XBOOLE_0:def_4;
hence  x in union (INTERSECTION (SFX,SFY)) by TARSKI:def_4; ::_thesis: verum
end;

theorem :: SETFAM_1:29
for SFX, SFY being set st SFX <> {} & SFY <> {} holds
(meet SFX) \/ (meet SFY) c= meet (UNION (SFX,SFY))
proof
let SFX, SFY be set ; ::_thesis: ( SFX <> {} & SFY <> {} implies (meet SFX) \/ (meet SFY) c= meet (UNION (SFX,SFY)) )
set y = the Element of SFX;
set z = the Element of SFY;
assume  ( SFX <> {} & SFY <> {} ) ; ::_thesis: (meet SFX) \/ (meet SFY) c= meet (UNION (SFX,SFY))
then A1: the Element of SFX \/ the Element of SFY in UNION (SFX,SFY) by Def4;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (meet SFX) \/ (meet SFY) or x in meet (UNION (SFX,SFY)) )
assume  x in (meet SFX) \/ (meet SFY) ; ::_thesis: x in meet (UNION (SFX,SFY))
then A2: ( x in meet SFX or x in meet SFY ) by XBOOLE_0:def_3;
 for Z being set st Z in UNION (SFX,SFY) holds
x in Z
proof
let Z be set ; ::_thesis: ( Z in UNION (SFX,SFY) implies x in Z )
assume  Z in UNION (SFX,SFY) ; ::_thesis: x in Z
then consider X, Y being set  such that
A3: ( X in SFX & Y in SFY ) and
A4: Z = X \/ Y by Def4;
 ( x in X or x in Y ) by A2, A3, Def1;
hence  x in Z by A4, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  x in meet (UNION (SFX,SFY)) by A1, Def1; ::_thesis: verum
end;

theorem :: SETFAM_1:30
for SFX, SFY being set holds meet (DIFFERENCE (SFX,SFY)) c= (meet SFX) \ (meet SFY)
proof
let SFX, SFY be set ; ::_thesis: meet (DIFFERENCE (SFX,SFY)) c= (meet SFX) \ (meet SFY)
percases ( SFX = {} or SFY = {} or ( SFX <> {} & SFY <> {} ) ) ;
supposeA1: ( SFX = {} or SFY = {} ) ; ::_thesis: meet (DIFFERENCE (SFX,SFY)) c= (meet SFX) \ (meet SFY)
now__::_thesis:_not_DIFFERENCE_(SFX,SFY)_<>_{}
assume  DIFFERENCE (SFX,SFY) <> {} ; ::_thesis: contradiction
then consider e being set  such that
A2: e in DIFFERENCE (SFX,SFY) by XBOOLE_0:def_1;
 ex X, Y being set st
( X in SFX & Y in SFY & e = X \ Y ) by A2, Def6;
hence  contradiction by A1; ::_thesis: verum
end;
then  meet (DIFFERENCE (SFX,SFY)) = {} by Def1;
hence  meet (DIFFERENCE (SFX,SFY)) c= (meet SFX) \ (meet SFY) by XBOOLE_1:2; ::_thesis: verum
end;
supposeA3: ( SFX <> {} & SFY <> {} ) ; ::_thesis: meet (DIFFERENCE (SFX,SFY)) c= (meet SFX) \ (meet SFY)
set z = the Element of SFX;
set y = the Element of SFY;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (DIFFERENCE (SFX,SFY)) or x in (meet SFX) \ (meet SFY) )
assume A4: x in meet (DIFFERENCE (SFX,SFY)) ; ::_thesis: x in (meet SFX) \ (meet SFY)
 for Z being set st Z in SFX holds
x in Z
proof
let Z be set ; ::_thesis: ( Z in SFX implies x in Z )
assume  Z in SFX ; ::_thesis: x in Z
then  Z \ the Element of SFY in DIFFERENCE (SFX,SFY) by A3, Def6;
then  x in Z \ the Element of SFY by A4, Def1;
hence  x in Z ; ::_thesis: verum
end;
then A5: x in meet SFX by A3, Def1;
 the Element of SFX \ the Element of SFY in DIFFERENCE (SFX,SFY) by A3, Def6;
then  x in the Element of SFX \ the Element of SFY by A4, Def1;
then  not x in the Element of SFY by XBOOLE_0:def_5;
then  not x in meet SFY by A3, Def1;
hence  x in (meet SFX) \ (meet SFY) by A5, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;

definition
let D be set ;
mode Subset-Family of D is Subset of (bool D);
end;


definition
let D be set ;
let F be Subset-Family of D;
:: original: union
redefine func union F ->  Subset of D;
coherence
 union F is Subset of D
proof
 union F c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F or x in D )
assume  x in union F ; ::_thesis: x in D
then  ex Z being set st
( x in Z & Z in F ) by TARSKI:def_4;
hence  x in D ; ::_thesis: verum
end;
hence  union F is Subset of D ; ::_thesis: verum
end;
end;

definition
let D be set ;
let F be Subset-Family of D;
:: original: meet
redefine func meet F ->  Subset of D;
coherence
 meet F is Subset of D
proof
 meet F c= D
proof
A1: meet F c= union F by Th2;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet F or x in D )
assume  x in meet F ; ::_thesis: x in D
then  x in union F by A1;
hence  x in D ; ::_thesis: verum
end;
hence  meet F is Subset of D ; ::_thesis: verum
end;
end;

theorem Th31: :: SETFAM_1:31
for D being set
for F, G being Subset-Family of D st ( for P being Subset of D holds
( P in F iff P in G ) ) holds
F = G
proof
let D be set ; ::_thesis: for F, G being Subset-Family of D st ( for P being Subset of D holds
( P in F iff P in G ) ) holds
F = G
let F, G be Subset-Family of D; ::_thesis: ( ( for P being Subset of D holds
( P in F iff P in G ) ) implies F = G )
assume A1: for P being Subset of D holds
( P in F iff P in G ) ; ::_thesis: F = G
thus  F c= G :: according to XBOOLE_0:def_10 ::_thesis: G c= F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in G )
assume  x in F ; ::_thesis: x in G
hence  x in G by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in G or x in F )
assume  x in G ; ::_thesis: x in F
hence  x in F by A1; ::_thesis: verum
end;

definition
let D be set ;
let F be Subset-Family of D;
func COMPLEMENT F ->  Subset-Family of D means :Def7: :: SETFAM_1:def 7
 for P being Subset of D holds
( P in it iff P ` in F );
existence
 ex b1 being Subset-Family of D st
for P being Subset of D holds
( P in b1 iff P ` in F )
proof
defpred S1[ Subset of D] means $1 ` in F;
thus  ex G being Subset-Family of D st
for P being Subset of D holds
( P in G iff S1[P] ) from SUBSET_1:sch_3(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of D st ( for P being Subset of D holds
( P in b1 iff P ` in F ) ) & ( for P being Subset of D holds
( P in b2 iff P ` in F ) ) holds
b1 = b2
proof
let G, H be Subset-Family of D; ::_thesis: ( ( for P being Subset of D holds
( P in G iff P ` in F ) ) & ( for P being Subset of D holds
( P in H iff P ` in F ) ) implies G = H )
assume that
A1: for P being Subset of D holds
( P in G iff P ` in F ) and
A2: for P being Subset of D holds
( P in H iff P ` in F ) ; ::_thesis: G = H
now__::_thesis:_for_P_being_Subset_of_D_holds_
(_P_in_G_iff_P_in_H_)
let P be Subset of D; ::_thesis: ( P in G iff P in H )
 ( P in G iff P ` in F ) by A1;
hence  ( P in G iff P in H ) by A2; ::_thesis: verum
end;
hence  G = H by Th31; ::_thesis: verum
end;
involutiveness
 for b1, b2 being Subset-Family of D st ( for P being Subset of D holds
( P in b1 iff P ` in b2 ) ) holds
for P being Subset of D holds
( P in b2 iff P ` in b1 )
proof
let F, G be Subset-Family of D; ::_thesis: ( ( for P being Subset of D holds
( P in F iff P ` in G ) ) implies for P being Subset of D holds
( P in G iff P ` in F ) )
assume A3: for P being Subset of D holds
( P in F iff P ` in G ) ; ::_thesis: for P being Subset of D holds
( P in G iff P ` in F )
let P be Subset of D; ::_thesis: ( P in G iff P ` in F )
 (P `) ` = P ;
hence  ( P in G iff P ` in F ) by A3; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines COMPLEMENT SETFAM_1:def_7_:_
 for D being set
for F, b3 being Subset-Family of D holds
( b3 = COMPLEMENT F iff for P being Subset of D holds
( P in b3 iff P ` in F ) );

theorem Th32: :: SETFAM_1:32
for D being set
for F being Subset-Family of D st F <> {} holds
COMPLEMENT F <> {}
proof
let D be set ; ::_thesis: for F being Subset-Family of D st F <> {} holds
COMPLEMENT F <> {}
let F be Subset-Family of D; ::_thesis: ( F <> {} implies COMPLEMENT F <> {} )
set X = the Element of F;
assume A1: F <> {} ; ::_thesis: COMPLEMENT F <> {}
then reconsider X = the Element of F as Subset of D by TARSKI:def_3;
 (X `) ` = X ;
hence  COMPLEMENT F <> {} by A1, Def7; ::_thesis: verum
end;

theorem :: SETFAM_1:33
for D being set
for F being Subset-Family of D st F <> {} holds
([#] D) \ (union F) = meet (COMPLEMENT F)
proof
let D be set ; ::_thesis: for F being Subset-Family of D st F <> {} holds
([#] D) \ (union F) = meet (COMPLEMENT F)
let F be Subset-Family of D; ::_thesis: ( F <> {} implies ([#] D) \ (union F) = meet (COMPLEMENT F) )
A1: for x being set st x in D holds
( ( for X being set st X in F holds
not x in X ) iff for Y being set st Y in COMPLEMENT F holds
x in Y )
proof
let x be set ; ::_thesis: ( x in D implies ( ( for X being set st X in F holds
not x in X ) iff for Y being set st Y in COMPLEMENT F holds
x in Y ) )
assume A2: x in D ; ::_thesis: ( ( for X being set st X in F holds
not x in X ) iff for Y being set st Y in COMPLEMENT F holds
x in Y )
thus  ( ( for X being set st X in F holds
not x in X ) implies for Y being set st Y in COMPLEMENT F holds
x in Y ) ::_thesis: ( ( for Y being set st Y in COMPLEMENT F holds
x in Y ) implies for X being set st X in F holds
not x in X )
proof
assume A3: for X being set st X in F holds
not x in X ; ::_thesis: for Y being set st Y in COMPLEMENT F holds
x in Y
let Y be set ; ::_thesis: ( Y in COMPLEMENT F implies x in Y )
assume A4: Y in COMPLEMENT F ; ::_thesis: x in Y
then reconsider Y = Y as Subset of D ;
 Y ` in F by A4, Def7;
then  not x in Y ` by A3;
hence  x in Y by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A5: for Y being set st Y in COMPLEMENT F holds
x in Y ; ::_thesis: for X being set st X in F holds
not x in X
let X be set ; ::_thesis: ( X in F implies not x in X )
assume A6: X in F ; ::_thesis: not x in X
then reconsider X = X as Subset of D ;
 (X `) ` = X ;
then  X ` in COMPLEMENT F by A6, Def7;
then  x in X ` by A5;
hence  not x in X by XBOOLE_0:def_5; ::_thesis: verum
end;
assume  F <> {} ; ::_thesis: ([#] D) \ (union F) = meet (COMPLEMENT F)
then A7: COMPLEMENT F <> {} by Th32;
A8: ([#] D) \ (union F) c= meet (COMPLEMENT F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ([#] D) \ (union F) or x in meet (COMPLEMENT F) )
assume A9: x in ([#] D) \ (union F) ; ::_thesis: x in meet (COMPLEMENT F)
then  not x in union F by XBOOLE_0:def_5;
then  for X being set st X in F holds
not x in X by TARSKI:def_4;
then  for Y being set st Y in COMPLEMENT F holds
x in Y by A1, A9;
hence  x in meet (COMPLEMENT F) by A7, Def1; ::_thesis: verum
end;
 meet (COMPLEMENT F) c= ([#] D) \ (union F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet (COMPLEMENT F) or x in ([#] D) \ (union F) )
assume A10: x in meet (COMPLEMENT F) ; ::_thesis: x in ([#] D) \ (union F)
then  for X being set st X in COMPLEMENT F holds
x in X by Def1;
then  for Y being set st x in Y holds
not Y in F by A1;
then  not x in union F by TARSKI:def_4;
hence  x in ([#] D) \ (union F) by A10, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  ([#] D) \ (union F) = meet (COMPLEMENT F) by A8, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: SETFAM_1:34
for D being set
for F being Subset-Family of D st F <> {} holds
union (COMPLEMENT F) = ([#] D) \ (meet F)
proof
let D be set ; ::_thesis: for F being Subset-Family of D st F <> {} holds
union (COMPLEMENT F) = ([#] D) \ (meet F)
let F be Subset-Family of D; ::_thesis: ( F <> {} implies union (COMPLEMENT F) = ([#] D) \ (meet F) )
assume A1: F <> {} ; ::_thesis: union (COMPLEMENT F) = ([#] D) \ (meet F)
A2: ([#] D) \ (meet F) c= union (COMPLEMENT F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ([#] D) \ (meet F) or x in union (COMPLEMENT F) )
assume A3: x in ([#] D) \ (meet F) ; ::_thesis: x in union (COMPLEMENT F)
then  not x in meet F by XBOOLE_0:def_5;
then consider X being set  such that
A4: X in F and
A5: not x in X by A1, Def1;
reconsider X = X as Subset of D by A4;
reconsider XX = X ` as set ;
A6: (X `) ` = X ;
 ex Y being set st
( x in Y & Y in COMPLEMENT F )
proof
take  XX ; ::_thesis: ( x in XX & XX in COMPLEMENT F )
thus  ( x in XX & XX in COMPLEMENT F ) by A3, A4, A5, A6, Def7, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  x in union (COMPLEMENT F) by TARSKI:def_4; ::_thesis: verum
end;
 union (COMPLEMENT F) c= ([#] D) \ (meet F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (COMPLEMENT F) or x in ([#] D) \ (meet F) )
assume A7: x in union (COMPLEMENT F) ; ::_thesis: x in ([#] D) \ (meet F)
then consider X being set  such that
A8: x in X and
A9: X in COMPLEMENT F by TARSKI:def_4;
reconsider X = X as Subset of D by A9;
reconsider XX = X ` as set ;
 ex Y being set st
( Y in F & not x in Y )
proof
take Y = XX; ::_thesis: ( Y in F & not x in Y )
thus  Y in F by A9, Def7; ::_thesis: not x in Y
thus  not x in Y by A8, XBOOLE_0:def_5; ::_thesis: verum
end;
then  not x in meet F by Def1;
hence  x in ([#] D) \ (meet F) by A7, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  union (COMPLEMENT F) = ([#] D) \ (meet F) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

begin

theorem :: SETFAM_1:35
for X being set
for F being Subset-Family of X
for P being Subset of X holds
( P ` in COMPLEMENT F iff P in F )
proof
let X be set ; ::_thesis: for F being Subset-Family of X
for P being Subset of X holds
( P ` in COMPLEMENT F iff P in F )
let F be Subset-Family of X; ::_thesis: for P being Subset of X holds
( P ` in COMPLEMENT F iff P in F )
let P be Subset of X; ::_thesis: ( P ` in COMPLEMENT F iff P in F )
 P = (P `) ` ;
hence  ( P ` in COMPLEMENT F iff P in F ) by Def7; ::_thesis: verum
end;

theorem Th36: :: SETFAM_1:36
for X being set
for F, G being Subset-Family of X st COMPLEMENT F c= COMPLEMENT G holds
F c= G
proof
let X be set ; ::_thesis: for F, G being Subset-Family of X st COMPLEMENT F c= COMPLEMENT G holds
F c= G
let F, G be Subset-Family of X; ::_thesis: ( COMPLEMENT F c= COMPLEMENT G implies F c= G )
assume A1: COMPLEMENT F c= COMPLEMENT G ; ::_thesis: F c= G
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in G )
assume A2: x in F ; ::_thesis: x in G
then reconsider A = x as Subset of X ;
 A in COMPLEMENT (COMPLEMENT F) by A2;
then  A ` in COMPLEMENT F by Def7;
then  (A `) ` in G by A1, Def7;
hence  x in G ; ::_thesis: verum
end;

theorem :: SETFAM_1:37
for X being set
for F, G being Subset-Family of X holds
( COMPLEMENT F c= G iff F c= COMPLEMENT G )
proof
let X be set ; ::_thesis: for F, G being Subset-Family of X holds
( COMPLEMENT F c= G iff F c= COMPLEMENT G )
let F, G be Subset-Family of X; ::_thesis: ( COMPLEMENT F c= G iff F c= COMPLEMENT G )
hereby  ::_thesis: ( F c= COMPLEMENT G implies COMPLEMENT F c= G )
assume  COMPLEMENT F c= G ; ::_thesis: F c= COMPLEMENT G
then  COMPLEMENT F c= COMPLEMENT (COMPLEMENT G) ;
hence  F c= COMPLEMENT G by Th36; ::_thesis: verum
end;
assume  F c= COMPLEMENT G ; ::_thesis: COMPLEMENT F c= G
then  COMPLEMENT (COMPLEMENT F) c= COMPLEMENT G ;
hence  COMPLEMENT F c= G by Th36; ::_thesis: verum
end;

theorem :: SETFAM_1:38
for X being set
for F, G being Subset-Family of X st COMPLEMENT F = COMPLEMENT G holds
F = G
proof
let X be set ; ::_thesis: for F, G being Subset-Family of X st COMPLEMENT F = COMPLEMENT G holds
F = G
let F, G be Subset-Family of X; ::_thesis: ( COMPLEMENT F = COMPLEMENT G implies F = G )
assume  COMPLEMENT F = COMPLEMENT G ; ::_thesis: F = G
hence F = COMPLEMENT (COMPLEMENT G)
.= G ;
::_thesis: verum
end;

theorem :: SETFAM_1:39
for X being set
for F, G being Subset-Family of X holds COMPLEMENT (F \/ G) = (COMPLEMENT F) \/ (COMPLEMENT G)
proof
let X be set ; ::_thesis: for F, G being Subset-Family of X holds COMPLEMENT (F \/ G) = (COMPLEMENT F) \/ (COMPLEMENT G)
let F, G be Subset-Family of X; ::_thesis: COMPLEMENT (F \/ G) = (COMPLEMENT F) \/ (COMPLEMENT G)
 for P being Subset of X holds
( P in (COMPLEMENT F) \/ (COMPLEMENT G) iff P ` in F \/ G )
proof
let P be Subset of X; ::_thesis: ( P in (COMPLEMENT F) \/ (COMPLEMENT G) iff P ` in F \/ G )
 ( ( ( not P in COMPLEMENT F & not P in COMPLEMENT G ) or P ` in F or P ` in G ) & ( ( not P ` in F & not P ` in G ) or P in COMPLEMENT F or P in COMPLEMENT G ) ) by Def7;
hence  ( P in (COMPLEMENT F) \/ (COMPLEMENT G) iff P ` in F \/ G ) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  COMPLEMENT (F \/ G) = (COMPLEMENT F) \/ (COMPLEMENT G) by Def7; ::_thesis: verum
end;

theorem :: SETFAM_1:40
for X being set
for F being Subset-Family of X st F = {X} holds
COMPLEMENT F = {{}}
proof
let X be set ; ::_thesis: for F being Subset-Family of X st F = {X} holds
COMPLEMENT F = {{}}
let F be Subset-Family of X; ::_thesis: ( F = {X} implies COMPLEMENT F = {{}} )
assume A1: F = {X} ; ::_thesis: COMPLEMENT F = {{}}
 {} c= X by XBOOLE_1:2;
then reconsider G = {{}} as Subset-Family of X by ZFMISC_1:31;
reconsider G = G as Subset-Family of X ;
 for P being Subset of X holds
( P in G iff P ` in F )
proof
let P be Subset of X; ::_thesis: ( P in G iff P ` in F )
hereby  ::_thesis: ( P ` in F implies P in G )
assume  P in G ; ::_thesis: P ` in F
then  P = {} X by TARSKI:def_1;
hence  P ` in F by A1, TARSKI:def_1; ::_thesis: verum
end;
assume  P ` in F ; ::_thesis: P in G
then A2: P ` = [#] X by A1, TARSKI:def_1;
P = (P `) `
.= {} by A2, XBOOLE_1:37 ;
hence  P in G by TARSKI:def_1; ::_thesis: verum
end;
hence  COMPLEMENT F = {{}} by Def7; ::_thesis: verum
end;

registration
let X be set ;
let F be empty Subset-Family of X;
cluster COMPLEMENT F ->  empty ;
coherence
 COMPLEMENT F is empty
proof
assume  not COMPLEMENT F is empty ; ::_thesis: contradiction
then  ex x being Subset of X st x in COMPLEMENT F by SUBSET_1:4;
hence  contradiction by Def7; ::_thesis: verum
end;
end;

definition
let IT be set ;
attrIT is with_non-empty_elements  means :Def8: :: SETFAM_1:def 8
 not {} in IT;
end;

:: deftheorem Def8 defines with_non-empty_elements SETFAM_1:def_8_:_
 for IT being set holds
( IT is with_non-empty_elements iff not {} in IT );

registration
cluster non empty with_non-empty_elements for set ;
existence
 ex b1 being set st
( not b1 is empty & b1 is with_non-empty_elements )
proof
take  {{{}}} ; ::_thesis: ( not {{{}}} is empty & {{{}}} is with_non-empty_elements )
thus  not {{{}}} is empty ; ::_thesis: {{{}}} is with_non-empty_elements
assume  {} in {{{}}} ; :: according to SETFAM_1:def_8 ::_thesis: contradiction
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let A be non empty set ;
cluster{A} ->  with_non-empty_elements ;
coherence
 {A} is with_non-empty_elements
proof
assume  {} in {A} ; :: according to SETFAM_1:def_8 ::_thesis: contradiction
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
let B be non empty set ;
cluster{A,B} ->  with_non-empty_elements ;
coherence
 {A,B} is with_non-empty_elements
proof
assume  {} in {A,B} ; :: according to SETFAM_1:def_8 ::_thesis: contradiction
hence  contradiction by TARSKI:def_2; ::_thesis: verum
end;
let C be non empty set ;
cluster{A,B,C} ->  with_non-empty_elements ;
coherence
 {A,B,C} is with_non-empty_elements
proof
assume  {} in {A,B,C} ; :: according to SETFAM_1:def_8 ::_thesis: contradiction
hence  contradiction by ENUMSET1:def_1; ::_thesis: verum
end;
let D be non empty set ;
cluster{A,B,C,D} ->  with_non-empty_elements ;
coherence
 {A,B,C,D} is with_non-empty_elements
proof
assume  {} in {A,B,C,D} ; :: according to SETFAM_1:def_8 ::_thesis: contradiction
hence  contradiction by ENUMSET1:def_2; ::_thesis: verum
end;
let E be non empty set ;
cluster{A,B,C,D,E} ->  with_non-empty_elements ;
coherence
 {A,B,C,D,E} is with_non-empty_elements
proof
assume  {} in {A,B,C,D,E} ; :: according to SETFAM_1:def_8 ::_thesis: contradiction
hence  contradiction by ENUMSET1:def_3; ::_thesis: verum
end;
let F be non empty set ;
cluster{A,B,C,D,E,F} ->  with_non-empty_elements ;
coherence
 {A,B,C,D,E,F} is with_non-empty_elements
proof
assume  {} in {A,B,C,D,E,F} ; :: according to SETFAM_1:def_8 ::_thesis: contradiction
hence  contradiction by ENUMSET1:def_4; ::_thesis: verum
end;
let G be non empty set ;
cluster{A,B,C,D,E,F,G} ->  with_non-empty_elements ;
coherence
 {A,B,C,D,E,F,G} is with_non-empty_elements
proof
assume  {} in {A,B,C,D,E,F,G} ; :: according to SETFAM_1:def_8 ::_thesis: contradiction
hence  contradiction by ENUMSET1:def_5; ::_thesis: verum
end;
let H be non empty set ;
cluster{A,B,C,D,E,F,G,H} ->  with_non-empty_elements ;
coherence
 {A,B,C,D,E,F,G,H} is with_non-empty_elements
proof
assume  {} in {A,B,C,D,E,F,G,H} ; :: according to SETFAM_1:def_8 ::_thesis: contradiction
hence  contradiction by ENUMSET1:def_6; ::_thesis: verum
end;
let I be non empty set ;
cluster{A,B,C,D,E,F,G,H,I} ->  with_non-empty_elements ;
coherence
 {A,B,C,D,E,F,G,H,I} is with_non-empty_elements
proof
assume  {} in {A,B,C,D,E,F,G,H,I} ; :: according to SETFAM_1:def_8 ::_thesis: contradiction
hence  contradiction by ENUMSET1:def_7; ::_thesis: verum
end;
let J be non empty set ;
cluster{A,B,C,D,E,F,G,H,I,J} ->  with_non-empty_elements ;
coherence
 {A,B,C,D,E,F,G,H,I,J} is with_non-empty_elements
proof
assume  {} in {A,B,C,D,E,F,G,H,I,J} ; :: according to SETFAM_1:def_8 ::_thesis: contradiction
hence  contradiction by ENUMSET1:def_8; ::_thesis: verum
end;
end;

registration
let A, B be with_non-empty_elements set ;
clusterA \/ B ->  with_non-empty_elements ;
coherence
 A \/ B is with_non-empty_elements
proof
 ( not {} in A & not {} in B ) by Def8;
then  not {} in A \/ B by XBOOLE_0:def_3;
hence  A \/ B is with_non-empty_elements by Def8; ::_thesis: verum
end;
end;

theorem :: SETFAM_1:41
for Y, Z, X being set st union Y c= Z & X in Y holds
X c= Z
proof
let Y, Z, X be set ; ::_thesis: ( union Y c= Z & X in Y implies X c= Z )
assume that
A1: union Y c= Z and
A2: X in Y ; ::_thesis: X c= Z
thus  X c= Z ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Z )
assume  x in X ; ::_thesis: x in Z
then  x in union Y by A2, TARSKI:def_4;
hence  x in Z by A1; ::_thesis: verum
end;
end;

theorem :: SETFAM_1:42
for A, B, X being set st X c= union (A \/ B) & ( for Y being set st Y in B holds
Y misses X ) holds
X c= union A
proof
let A, B, X be set ; ::_thesis: ( X c= union (A \/ B) & ( for Y being set st Y in B holds
Y misses X ) implies X c= union A )
assume  X c= union (A \/ B) ; ::_thesis: ( ex Y being set st
( Y in B & not Y misses X ) or X c= union A )
then  X c= (union (A \/ B)) /\ X by XBOOLE_1:19;
then  X c= ((union A) \/ (union B)) /\ X by ZFMISC_1:78;
then A1: X c= ((union A) /\ X) \/ ((union B) /\ X) by XBOOLE_1:23;
assume  for Y being set st Y in B holds
Y misses X ; ::_thesis: X c= union A
then  union B misses X by ZFMISC_1:80;
then A2: (union B) /\ X = {} by XBOOLE_0:def_7;
 (union A) /\ X c= union A by XBOOLE_1:17;
hence  X c= union A by A2, A1, XBOOLE_1:1; ::_thesis: verum
end;

definition
let M be set ;
let B be Subset-Family of M;
func Intersect B ->  Subset of M equals :Def9: :: SETFAM_1:def 9
 meet B if B <> {}
otherwise M;
coherence
 ( ( B <> {} implies meet B is Subset of M ) & ( not B <> {} implies M is Subset of M ) )
proof
 M c= M ;
hence  ( ( B <> {} implies meet B is Subset of M ) & ( not B <> {} implies M is Subset of M ) ) ; ::_thesis: verum
end;
consistency
 for b1 being Subset of M holds verum ;
end;

:: deftheorem Def9 defines Intersect SETFAM_1:def_9_:_
 for M being set
for B being Subset-Family of M holds
( ( B <> {} implies Intersect B = meet B ) & ( not B <> {} implies Intersect B = M ) );

theorem Th43: :: SETFAM_1:43
for X, x being set
for R being Subset-Family of X st x in X holds
( x in Intersect R iff for Y being set st Y in R holds
x in Y )
proof
let X, x be set ; ::_thesis: for R being Subset-Family of X st x in X holds
( x in Intersect R iff for Y being set st Y in R holds
x in Y )
let R be Subset-Family of X; ::_thesis: ( x in X implies ( x in Intersect R iff for Y being set st Y in R holds
x in Y ) )
assume A1: x in X ; ::_thesis: ( x in Intersect R iff for Y being set st Y in R holds
x in Y )
hereby  ::_thesis: ( ( for Y being set st Y in R holds
x in Y ) implies x in Intersect R )
assume A2: x in Intersect R ; ::_thesis: for Y being set st Y in R holds
x in Y
let Y be set ; ::_thesis: ( Y in R implies x in Y )
assume A3: Y in R ; ::_thesis: x in Y
then  Intersect R = meet R by Def9;
hence  x in Y by A2, A3, Def1; ::_thesis: verum
end;
assume A4: for Y being set st Y in R holds
x in Y ; ::_thesis: x in Intersect R
percases ( R <> {} or R = {} ) ;
supposeA5: R <> {} ; ::_thesis: x in Intersect R
then  x in meet R by A4, Def1;
hence  x in Intersect R by A5, Def9; ::_thesis: verum
end;
suppose R = {} ; ::_thesis: x in Intersect R
hence  x in Intersect R by A1, Def9; ::_thesis: verum
end;
end;
end;

theorem :: SETFAM_1:44
for X being set
for H, J being Subset-Family of X st H c= J holds
Intersect J c= Intersect H
proof
let X be set ; ::_thesis: for H, J being Subset-Family of X st H c= J holds
Intersect J c= Intersect H
let H, J be Subset-Family of X; ::_thesis: ( H c= J implies Intersect J c= Intersect H )
assume A1: H c= J ; ::_thesis: Intersect J c= Intersect H
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersect J or x in Intersect H )
assume A2: x in Intersect J ; ::_thesis: x in Intersect H
then  for Y being set st Y in H holds
x in Y by A1, Th43;
hence  x in Intersect H by A2, Th43; ::_thesis: verum
end;

registration
let X be non empty with_non-empty_elements set ;
cluster  ->  non empty for Element of X;
coherence
 for b1 being Element of X holds not b1 is empty by Def8;
end;

definition
let E be set ;
attrE is empty-membered  means :Def10: :: SETFAM_1:def 10
 for x being non empty set holds not x in E;
end;

:: deftheorem Def10 defines empty-membered SETFAM_1:def_10_:_
 for E being set holds
( E is empty-membered iff for x being non empty set holds not x in E );

notation
let E be set ;
antonym  with_non-empty_element E for  empty-membered ;
end;

registration
cluster with_non-empty_element for set ;
existence
 ex b1 being set st b1 is with_non-empty_element
proof
take  {{{}}} ; ::_thesis: {{{}}} is with_non-empty_element
take  {{}} ; :: according to SETFAM_1:def_10 ::_thesis: {{}} in {{{}}}
thus  {{}} in {{{}}} by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
cluster with_non-empty_element  ->  non empty for set ;
coherence
 for b1 being set st b1 is with_non-empty_element holds
not b1 is empty
proof
let X be set ; ::_thesis: ( X is with_non-empty_element implies not X is empty )
assume  X is with_non-empty_element ; ::_thesis: not X is empty
then  ex x being non empty set st x in X by Def10;
hence  not X is empty ; ::_thesis: verum
end;
end;

registration
let X be with_non-empty_element set ;
cluster non empty for Element of X;
existence
 not for b1 being Element of X holds b1 is empty
proof
 ex x being non empty set st x in X by Def10;
hence  not for b1 being Element of X holds b1 is empty ; ::_thesis: verum
end;
end;

registration
let D be non empty with_non-empty_elements set ;
cluster union D ->  non empty ;
coherence
 not union D is empty
proof
set d = the Element of D;
 the Element of D c= union D by ZFMISC_1:74;
hence  not union D is empty ; ::_thesis: verum
end;
end;

registration
cluster non empty with_non-empty_elements  ->  with_non-empty_element for set ;
coherence
 for b1 being set st not b1 is empty & b1 is with_non-empty_elements holds
b1 is with_non-empty_element
proof
let X be set ; ::_thesis: ( not X is empty & X is with_non-empty_elements implies X is with_non-empty_element )
assume that
A1: not X is empty and
A2: X is with_non-empty_elements ; ::_thesis: X is with_non-empty_element
consider x being Element of X such that
A3: x in [#] X by A1, SUBSET_1:4;
reconsider x = x as non empty set by A2, A3;
take  x ; :: according to SETFAM_1:def_10 ::_thesis: x in X
thus  x in X by A3; ::_thesis: verum
end;
end;

definition
let X be set ;
mode Cover of X ->  set  means :Def11: :: SETFAM_1:def 11
X c= union it;
existence
 ex b1 being set st X c= union b1
proof
take  {X} ; ::_thesis: X c= union {X}
thus  X c= union {X} by ZFMISC_1:25; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines Cover SETFAM_1:def_11_:_
 for X being set
for b2 being set holds
( b2 is Cover of X iff X c= union b2 );

theorem :: SETFAM_1:45
for X being set
for F being Subset-Family of X holds
( F is Cover of X iff union F = X )
proof
let X be set ; ::_thesis: for F being Subset-Family of X holds
( F is Cover of X iff union F = X )
let F be Subset-Family of X; ::_thesis: ( F is Cover of X iff union F = X )
thus  ( F is Cover of X implies union F = X ) ::_thesis: ( union F = X implies F is Cover of X )
proof
assume A1: F is Cover of X ; ::_thesis: union F = X
thus  union F c= X ; :: according to XBOOLE_0:def_10 ::_thesis: X c= union F
thus  X c= union F by A1, Def11; ::_thesis: verum
end;
thus  ( union F = X implies F is Cover of X ) by Def11; ::_thesis: verum
end;

theorem Th46: :: SETFAM_1:46
for X being set holds {{}} is Subset-Family of X
proof
let X be set ; ::_thesis: {{}} is Subset-Family of X
 {} c= X by XBOOLE_1:2;
hence  {{}} is Subset-Family of X by ZFMISC_1:31; ::_thesis: verum
end;

definition
let X be set ;
let F be Subset-Family of X;
attrF is with_proper_subsets  means :Def12: :: SETFAM_1:def 12
 not X in F;
end;

:: deftheorem Def12 defines with_proper_subsets SETFAM_1:def_12_:_
 for X being set
for F being Subset-Family of X holds
( F is with_proper_subsets iff not X in F );

theorem :: SETFAM_1:47
for TS being set
for F, G being Subset-Family of TS st F is with_proper_subsets & G c= F holds
G is with_proper_subsets
proof
let TS be set ; ::_thesis: for F, G being Subset-Family of TS st F is with_proper_subsets & G c= F holds
G is with_proper_subsets
let F, G be Subset-Family of TS; ::_thesis: ( F is with_proper_subsets & G c= F implies G is with_proper_subsets )
assume A1: ( F is with_proper_subsets & G c= F ) ; ::_thesis: G is with_proper_subsets
assume  not G is with_proper_subsets ; ::_thesis: contradiction
then  TS in G by Def12;
hence  contradiction by A1, Def12; ::_thesis: verum
end;

registration
let TS be non empty set ;
cluster with_proper_subsets for Element of bool (bool TS);
existence
 ex b1 being Subset-Family of TS st b1 is with_proper_subsets
proof
reconsider F = {{}} as Subset-Family of TS by Th46;
take  F ; ::_thesis: F is with_proper_subsets
assume  TS in F ; :: according to SETFAM_1:def_12 ::_thesis: contradiction
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
end;

theorem :: SETFAM_1:48
for TS being non empty set
for A, B being with_proper_subsets Subset-Family of TS holds A \/ B is with_proper_subsets
proof
let TS be non empty set ; ::_thesis: for A, B being with_proper_subsets Subset-Family of TS holds A \/ B is with_proper_subsets
let A, B be with_proper_subsets Subset-Family of TS; ::_thesis: A \/ B is with_proper_subsets
assume  TS in A \/ B ; :: according to SETFAM_1:def_12 ::_thesis: contradiction
then  ( TS in A or TS in B ) by XBOOLE_0:def_3;
hence  contradiction by Def12; ::_thesis: verum
end;

registration
cluster non trivial  ->  with_non-empty_element for set ;
coherence
 for b1 being set st not b1 is trivial holds
b1 is with_non-empty_element
proof
let W be set ; ::_thesis: ( not W is trivial implies W is with_non-empty_element )
assume  not W is trivial ; ::_thesis: W is with_non-empty_element
then consider w1, w2 being set  such that
A1: ( w1 in W & w2 in W ) and
A2: w1 <> w2 by ZFMISC_1:def_10;
 ( w1 <> {} or w2 <> {} ) by A2;
hence  W is with_non-empty_element by A1, Def10; ::_thesis: verum
end;
end;

definition
let X be set ;
:: original: bool
redefine func bool X ->  Subset-Family of X;
coherence
 bool X is Subset-Family of X by ZFMISC_1:def_1;
end;

theorem :: SETFAM_1:49
for A being non empty set
for b being set st A <> {b} holds
ex a being Element of A st a <> b
proof
let A be non empty set ; ::_thesis: for b being set st A <> {b} holds
ex a being Element of A st a <> b
let b be set ; ::_thesis: ( A <> {b} implies ex a being Element of A st a <> b )
assume A1: A <> {b} ; ::_thesis: ex a being Element of A st a <> b
assume A2: for a being Element of A holds a = b ; ::_thesis: contradiction
now__::_thesis:_for_a_being_set_holds_
(_(_a_in_A_implies_a_=_b_)_&_(_a_=_b_implies_a_in_A_)_)
set a0 = the Element of A;
let a be set ; ::_thesis: ( ( a in A implies a = b ) & ( a = b implies a in A ) )
thus  ( a in A implies a = b ) by A2; ::_thesis: ( a = b implies a in A )
assume A3: a = b ; ::_thesis: a in A
 the Element of A = b by A2;
hence  a in A by A3; ::_thesis: verum
end;
hence  contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;