:: SUBSET_1 semantic presentation

begin


registration
let X be set ;
cluster bool X ->  non empty ;
coherence
 not bool X is empty by ZFMISC_1:def_1;
end;

registration
let x1, x2, x3 be set ;
cluster{x1,x2,x3} ->  non empty ;
coherence
 not {x1,x2,x3} is empty by ENUMSET1:def_1;
let x4 be set ;
cluster{x1,x2,x3,x4} ->  non empty ;
coherence
 not {x1,x2,x3,x4} is empty by ENUMSET1:def_2;
let x5 be set ;
cluster{x1,x2,x3,x4,x5} ->  non empty ;
coherence
 not {x1,x2,x3,x4,x5} is empty by ENUMSET1:def_3;
let x6 be set ;
cluster{x1,x2,x3,x4,x5,x6} ->  non empty ;
coherence
 not {x1,x2,x3,x4,x5,x6} is empty by ENUMSET1:def_4;
let x7 be set ;
cluster{x1,x2,x3,x4,x5,x6,x7} ->  non empty ;
coherence
 not {x1,x2,x3,x4,x5,x6,x7} is empty by ENUMSET1:def_5;
let x8 be set ;
cluster{x1,x2,x3,x4,x5,x6,x7,x8} ->  non empty ;
coherence
 not {x1,x2,x3,x4,x5,x6,x7,x8} is empty by ENUMSET1:def_6;
let x9 be set ;
cluster{x1,x2,x3,x4,x5,x6,x7,x8,x9} ->  non empty ;
coherence
 not {x1,x2,x3,x4,x5,x6,x7,x8,x9} is empty by ENUMSET1:def_7;
let x10 be set ;
cluster{x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} ->  non empty ;
coherence
 not {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} is empty by ENUMSET1:def_8;
end;

definition
let X be set ;
mode Element of X ->  set  means :Def1: :: SUBSET_1:def 1
it in X if  not X is empty
otherwise it is empty ;
existence
 ( ( not X is empty implies ex b1 being set st b1 in X ) & ( X is empty implies ex b1 being set st b1 is empty ) ) by XBOOLE_0:def_1;
consistency
 for b1 being set holds verum ;
sethood
 ( ( not X is empty & ex b1 being set st
for b2 being set st b2 in X holds
b2 in b1 ) or ( X is empty & ex b1 being set st
for b2 being set st b2 is empty holds
b2 in b1 ) )
proof
percases ( not X is empty or X is empty ) ;
case not X is empty ; ::_thesis: ex b1 being set st
for b2 being set st b2 in X holds
b2 in b1
take  X ; ::_thesis: for b1 being set st b1 in X holds
b1 in X
thus  for b1 being set st b1 in X holds
b1 in X ; ::_thesis: verum
end;
case X is empty ; ::_thesis: ex b1 being set st
for b2 being set st b2 is empty holds
b2 in b1
take  {{}} ; ::_thesis: for b1 being set st b1 is empty holds
b1 in {{}}
let y be set ; ::_thesis: ( y is empty implies y in {{}} )
thus  ( y is empty implies y in {{}} ) by TARSKI:def_1; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def1 defines Element SUBSET_1:def_1_:_
 for X being set
for b2 being set holds
( ( not X is empty implies ( b2 is Element of X iff b2 in X ) ) & ( X is empty implies ( b2 is Element of X iff b2 is empty ) ) );

definition
let X be set ;
mode Subset of X is Element of bool X;
end;

registration
let X be non empty set ;
cluster non empty for Element of bool X;
existence
 not for b1 being Subset of X holds b1 is empty
proof
 X in bool X by ZFMISC_1:def_1;
then  X is Subset of X by Def1;
hence  not for b1 being Subset of X holds b1 is empty ; ::_thesis: verum
end;
end;

registration
let X1, X2 be non empty set ;
cluster[:X1,X2:] ->  non empty ;
coherence
 not [:X1,X2:] is empty
proof
consider x2 being set  such that
A1: x2 in X2 by XBOOLE_0:def_1;
consider x1 being set  such that
A2: x1 in X1 by XBOOLE_0:def_1;
 [x1,x2] in [:X1,X2:] by A2, A1, ZFMISC_1:def_2;
hence  not [:X1,X2:] is empty ; ::_thesis: verum
end;
end;

registration
let X1, X2, X3 be non empty set ;
cluster[:X1,X2,X3:] ->  non empty ;
coherence
 not [:X1,X2,X3:] is empty ;
end;

registration
let X1, X2, X3, X4 be non empty set ;
cluster[:X1,X2,X3,X4:] ->  non empty ;
coherence
 not [:X1,X2,X3,X4:] is empty ;
end;

definition
let D be non empty set ;
let X be non empty Subset of D;
:: original: Element
redefine mode Element of X ->  Element of D;
coherence
 for b1 being Element of X holds b1 is Element of D
proof
let x be Element of X; ::_thesis: x is Element of D
 X in bool D by Def1;
then A1: X c= D by ZFMISC_1:def_1;
 x in X by Def1;
then  x in D by A1, TARSKI:def_3;
hence  x is Element of D by Def1; ::_thesis: verum
end;
end;

Lm1:  for E being set
for X being Subset of E
for x being set st x in X holds
x in E
proof
let E be set ; ::_thesis: for X being Subset of E
for x being set st x in X holds
x in E
let X be Subset of E; ::_thesis: for x being set st x in X holds
x in E
let x be set ; ::_thesis: ( x in X implies x in E )
assume A1: x in X ; ::_thesis: x in E
 X in bool E by Def1;
then  X c= E by ZFMISC_1:def_1;
hence  x in E by A1, TARSKI:def_3; ::_thesis: verum
end;

registration
let E be set ;
cluster empty for Element of bool E;
existence
 ex b1 being Subset of E st b1 is empty
proof
 {} c= E by XBOOLE_1:2;
then  {} in bool E by ZFMISC_1:def_1;
then  {} is Subset of E by Def1;
hence  ex b1 being Subset of E st b1 is empty ; ::_thesis: verum
end;
end;

definition
let E be set ;
func {} E ->  Subset of E equals :: SUBSET_1:def 2
 {} ;
coherence
 {} is Subset of E
proof
 {} c= E by XBOOLE_1:2;
then  {} in bool E by ZFMISC_1:def_1;
hence  {} is Subset of E by Def1; ::_thesis: verum
end;
correctness
;
func [#] E ->  Subset of E equals :: SUBSET_1:def 3
E;
coherence
 E is Subset of E
proof
 E in bool E by ZFMISC_1:def_1;
hence  E is Subset of E by Def1; ::_thesis: verum
end;
correctness
;
end;

:: deftheorem  defines {} SUBSET_1:def_2_:_
 for E being set holds {} E = {} ;

:: deftheorem  defines [#] SUBSET_1:def_3_:_
 for E being set holds [#] E = E;

registration
let E be set ;
cluster {} E ->  empty ;
coherence
 {} E is empty ;
end;

theorem :: SUBSET_1:1
for X being set holds {} is Subset of X
proof
let X be set ; ::_thesis: {} is Subset of X
 {} X = {} ;
hence  {} is Subset of X ; ::_thesis: verum
end;


theorem Th2: :: SUBSET_1:2
for E being set
for A, B being Subset of E st ( for x being Element of E st x in A holds
x in B ) holds
A c= B
proof
let E be set ; ::_thesis: for A, B being Subset of E st ( for x being Element of E st x in A holds
x in B ) holds
A c= B
let A, B be Subset of E; ::_thesis: ( ( for x being Element of E st x in A holds
x in B ) implies A c= B )
assume A1: for x being Element of E st x in A holds
x in B ; ::_thesis: A c= B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume A2: x in A ; ::_thesis: x in B
then  x in E by Lm1;
then  x is Element of E by Def1;
hence  x in B by A1, A2; ::_thesis: verum
end;

theorem Th3: :: SUBSET_1:3
for E being set
for A, B being Subset of E st ( for x being Element of E holds
( x in A iff x in B ) ) holds
A = B
proof
let E be set ; ::_thesis: for A, B being Subset of E st ( for x being Element of E holds
( x in A iff x in B ) ) holds
A = B
let A, B be Subset of E; ::_thesis: ( ( for x being Element of E holds
( x in A iff x in B ) ) implies A = B )
assume  for x being Element of E holds
( x in A iff x in B ) ; ::_thesis: A = B
hence  ( A c= B & B c= A ) by Th2; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;

theorem Th4: :: SUBSET_1:4
for E being set
for A being Subset of E st A <> {} holds
ex x being Element of E st x in A
proof
let E be set ; ::_thesis: for A being Subset of E st A <> {} holds
ex x being Element of E st x in A
let A be Subset of E; ::_thesis: ( A <> {} implies ex x being Element of E st x in A )
assume  A <> {} ; ::_thesis: ex x being Element of E st x in A
then consider x being set  such that
A1: x in A by XBOOLE_0:def_1;
 x in E by A1, Lm1;
then  x is Element of E by Def1;
hence  ex x being Element of E st x in A by A1; ::_thesis: verum
end;

definition
let E be set ;
let A be Subset of E;
funcA `  ->  Subset of E equals :: SUBSET_1:def 4
E \ A;
coherence
 E \ A is Subset of E
proof
 E \ A c= E by XBOOLE_1:36;
then  E \ A in bool E by ZFMISC_1:def_1;
hence  E \ A is Subset of E by Def1; ::_thesis: verum
end;
correctness
;
involutiveness
 for b1, b2 being Subset of E st b1 = E \ b2 holds
b2 = E \ b1
proof
let S, T be Subset of E; ::_thesis: ( S = E \ T implies T = E \ S )
assume A1: S = E \ T ; ::_thesis: T = E \ S
 T in bool E by Def1;
then  T c= E by ZFMISC_1:def_1;
hence T = {} \/ (E /\ T) by XBOOLE_1:28
.= (E \ E) \/ (E /\ T) by XBOOLE_1:37
.= E \ S by A1, XBOOLE_1:52 ;
::_thesis: verum
end;
let B be Subset of E;
:: original: \/
redefine funcA \/ B ->  Subset of E;
coherence
 A \/ B is Subset of E
proof
 B in bool E by Def1;
then A2: B c= E by ZFMISC_1:def_1;
 A in bool E by Def1;
then  A c= E by ZFMISC_1:def_1;
then  A \/ B c= E by A2, XBOOLE_1:8;
then  A \/ B in bool E by ZFMISC_1:def_1;
hence  A \/ B is Subset of E by Def1; ::_thesis: verum
end;
:: original: \+\
redefine funcA \+\ B ->  Subset of E;
coherence
 A \+\ B is Subset of E
proof
 B in bool E by Def1;
then  ( B \ A c= B & B c= E ) by XBOOLE_1:36, ZFMISC_1:def_1;
then A3: B \ A c= E by XBOOLE_1:1;
 A in bool E by Def1;
then  ( A \ B c= A & A c= E ) by XBOOLE_1:36, ZFMISC_1:def_1;
then  A \ B c= E by XBOOLE_1:1;
then  (A \ B) \/ (B \ A) c= E by A3, XBOOLE_1:8;
then  A \+\ B in bool E by ZFMISC_1:def_1;
hence  A \+\ B is Subset of E by Def1; ::_thesis: verum
end;
end;

:: deftheorem  defines ` SUBSET_1:def_4_:_
 for E being set
for A being Subset of E holds A ` = E \ A;

definition
let X, Y be set ;
:: original: \
redefine funcX \ Y ->  Subset of X;
coherence
 X \ Y is Subset of X
proof
 X \ Y c= X by XBOOLE_1:36;
then  X \ Y in bool X by ZFMISC_1:def_1;
hence  X \ Y is Subset of X by Def1; ::_thesis: verum
end;
end;

definition
let E be set ;
let A be Subset of E;
let X be set ;
:: original: \
redefine funcA \ X ->  Subset of E;
coherence
 A \ X is Subset of E
proof
 A in bool E by Def1;
then  ( A \ X c= A & A c= E ) by XBOOLE_1:36, ZFMISC_1:def_1;
then  A \ X c= E by XBOOLE_1:1;
then  A \ X in bool E by ZFMISC_1:def_1;
hence  A \ X is Subset of E by Def1; ::_thesis: verum
end;
end;

definition
let E be set ;
let A be Subset of E;
let X be set ;
:: original: /\
redefine funcA /\ X ->  Subset of E;
coherence
 A /\ X is Subset of E
proof
 A in bool E by Def1;
then  ( A /\ X c= A & A c= E ) by XBOOLE_1:17, ZFMISC_1:def_1;
then  A /\ X c= E by XBOOLE_1:1;
then  A /\ X in bool E by ZFMISC_1:def_1;
hence  A /\ X is Subset of E by Def1; ::_thesis: verum
end;
end;

definition
let E, X be set ;
let A be Subset of E;
:: original: /\
redefine funcX /\ A ->  Subset of E;
coherence
 X /\ A is Subset of E
proof
 A /\ X is Subset of E ;
hence  X /\ A is Subset of E ; ::_thesis: verum
end;
end;

theorem :: SUBSET_1:5
for E being set
for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( x in B or x in C ) ) ) holds
A = B \/ C
proof
let E be set ; ::_thesis: for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( x in B or x in C ) ) ) holds
A = B \/ C
let A, B, C be Subset of E; ::_thesis: ( ( for x being Element of E holds
( x in A iff ( x in B or x in C ) ) ) implies A = B \/ C )
assume A1: for x being Element of E holds
( x in A iff ( x in B or x in C ) ) ; ::_thesis: A = B \/ C
now__::_thesis:_for_x_being_Element_of_E_st_x_in_A_holds_
x_in_B_\/_C
let x be Element of E; ::_thesis: ( x in A implies x in B \/ C )
assume  x in A ; ::_thesis: x in B \/ C
then  ( x in B or x in C ) by A1;
hence  x in B \/ C by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  A c= B \/ C by Th2; :: according to XBOOLE_0:def_10 ::_thesis: B \/ C c= A
now__::_thesis:_for_x_being_Element_of_E_st_x_in_B_\/_C_holds_
x_in_A
let x be Element of E; ::_thesis: ( x in B \/ C implies x in A )
assume  x in B \/ C ; ::_thesis: x in A
then  ( x in B or x in C ) by XBOOLE_0:def_3;
hence  x in A by A1; ::_thesis: verum
end;
hence  B \/ C c= A by Th2; ::_thesis: verum
end;

theorem :: SUBSET_1:6
for E being set
for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( x in B & x in C ) ) ) holds
A = B /\ C
proof
let E be set ; ::_thesis: for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( x in B & x in C ) ) ) holds
A = B /\ C
let A, B, C be Subset of E; ::_thesis: ( ( for x being Element of E holds
( x in A iff ( x in B & x in C ) ) ) implies A = B /\ C )
assume A1: for x being Element of E holds
( x in A iff ( x in B & x in C ) ) ; ::_thesis: A = B /\ C
now__::_thesis:_for_x_being_Element_of_E_st_x_in_A_holds_
x_in_B_/\_C
let x be Element of E; ::_thesis: ( x in A implies x in B /\ C )
assume  x in A ; ::_thesis: x in B /\ C
then  ( x in B & x in C ) by A1;
hence  x in B /\ C by XBOOLE_0:def_4; ::_thesis: verum
end;
hence  A c= B /\ C by Th2; :: according to XBOOLE_0:def_10 ::_thesis: B /\ C c= A
now__::_thesis:_for_x_being_Element_of_E_st_x_in_B_/\_C_holds_
x_in_A
let x be Element of E; ::_thesis: ( x in B /\ C implies x in A )
assume  x in B /\ C ; ::_thesis: x in A
then  ( x in B & x in C ) by XBOOLE_0:def_4;
hence  x in A by A1; ::_thesis: verum
end;
hence  B /\ C c= A by Th2; ::_thesis: verum
end;

theorem :: SUBSET_1:7
for E being set
for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( x in B & not x in C ) ) ) holds
A = B \ C
proof
let E be set ; ::_thesis: for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( x in B & not x in C ) ) ) holds
A = B \ C
let A, B, C be Subset of E; ::_thesis: ( ( for x being Element of E holds
( x in A iff ( x in B & not x in C ) ) ) implies A = B \ C )
assume A1: for x being Element of E holds
( x in A iff ( x in B & not x in C ) ) ; ::_thesis: A = B \ C
now__::_thesis:_for_x_being_Element_of_E_st_x_in_A_holds_
x_in_B_\_C
let x be Element of E; ::_thesis: ( x in A implies x in B \ C )
assume  x in A ; ::_thesis: x in B \ C
then  ( x in B & not x in C ) by A1;
hence  x in B \ C by XBOOLE_0:def_5; ::_thesis: verum
end;
hence  A c= B \ C by Th2; :: according to XBOOLE_0:def_10 ::_thesis: B \ C c= A
now__::_thesis:_for_x_being_Element_of_E_st_x_in_B_\_C_holds_
x_in_A
let x be Element of E; ::_thesis: ( x in B \ C implies x in A )
assume  x in B \ C ; ::_thesis: x in A
then  ( x in B & not x in C ) by XBOOLE_0:def_5;
hence  x in A by A1; ::_thesis: verum
end;
hence  B \ C c= A by Th2; ::_thesis: verum
end;

theorem :: SUBSET_1:8
for E being set
for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) ) ) holds
A = B \+\ C
proof
let E be set ; ::_thesis: for A, B, C being Subset of E st ( for x being Element of E holds
( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) ) ) holds
A = B \+\ C
let A, B, C be Subset of E; ::_thesis: ( ( for x being Element of E holds
( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) ) ) implies A = B \+\ C )
assume A1: for x being Element of E holds
( x in A iff ( ( x in B & not x in C ) or ( x in C & not x in B ) ) ) ; ::_thesis: A = B \+\ C
now__::_thesis:_for_x_being_Element_of_E_st_x_in_A_holds_
x_in_B_\+\_C
let x be Element of E; ::_thesis: ( x in A implies x in B \+\ C )
assume  x in A ; ::_thesis: x in B \+\ C
then  ( ( x in B & not x in C ) or ( x in C & not x in B ) ) by A1;
then  ( x in B \ C or x in C \ B ) by XBOOLE_0:def_5;
hence  x in B \+\ C by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  A c= B \+\ C by Th2; :: according to XBOOLE_0:def_10 ::_thesis: B \+\ C c= A
now__::_thesis:_for_x_being_Element_of_E_st_x_in_B_\+\_C_holds_
x_in_A
let x be Element of E; ::_thesis: ( x in B \+\ C implies x in A )
assume  x in B \+\ C ; ::_thesis: x in A
then  ( x in B \ C or x in C \ B ) by XBOOLE_0:def_3;
then  ( ( x in B & not x in C ) or ( x in C & not x in B ) ) by XBOOLE_0:def_5;
hence  x in A by A1; ::_thesis: verum
end;
hence  B \+\ C c= A by Th2; ::_thesis: verum
end;

theorem :: SUBSET_1:9
for E being set holds [#] E = ({} E) ` ;

theorem Th10: :: SUBSET_1:10
for E being set
for A being Subset of E holds A \/ (A `) = [#] E
proof
let E be set ; ::_thesis: for A being Subset of E holds A \/ (A `) = [#] E
let A be Subset of E; ::_thesis: A \/ (A `) = [#] E
 A in bool E by Def1;
then  A c= E by ZFMISC_1:def_1;
hence  A \/ (A `) = [#] E by XBOOLE_1:45; ::_thesis: verum
end;

theorem :: SUBSET_1:11
for E being set
for A being Subset of E holds A \/ ([#] E) = [#] E
proof
let E be set ; ::_thesis: for A being Subset of E holds A \/ ([#] E) = [#] E
let A be Subset of E; ::_thesis: A \/ ([#] E) = [#] E
 A in bool E by Def1;
then  A c= E by ZFMISC_1:def_1;
hence  A \/ ([#] E) = [#] E by XBOOLE_1:12; ::_thesis: verum
end;

theorem Th12: :: SUBSET_1:12
for E being set
for A, B being Subset of E holds
( A c= B iff B ` c= A ` )
proof
let E be set ; ::_thesis: for A, B being Subset of E holds
( A c= B iff B ` c= A ` )
let A, B be Subset of E; ::_thesis: ( A c= B iff B ` c= A ` )
thus  ( A c= B implies B ` c= A ` ) by XBOOLE_1:34; ::_thesis: ( B ` c= A ` implies A c= B )
A1: E \ (B `) = (B `) `
.= B ;
E \ (A `) = (A `) `
.= A ;
hence  ( B ` c= A ` implies A c= B ) by A1, XBOOLE_1:34; ::_thesis: verum
end;

theorem :: SUBSET_1:13
for E being set
for A, B being Subset of E holds A \ B = A /\ (B `)
proof
let E be set ; ::_thesis: for A, B being Subset of E holds A \ B = A /\ (B `)
let A, B be Subset of E; ::_thesis: A \ B = A /\ (B `)
 A in bool E by Def1;
then A1: A c= E by ZFMISC_1:def_1;
thus A /\ (B `) = (A /\ E) \ B by XBOOLE_1:49
.= A \ B by A1, XBOOLE_1:28 ; ::_thesis: verum
end;

theorem :: SUBSET_1:14
for E being set
for A, B being Subset of E holds (A \ B) ` = (A `) \/ B
proof
let E be set ; ::_thesis: for A, B being Subset of E holds (A \ B) ` = (A `) \/ B
let A, B be Subset of E; ::_thesis: (A \ B) ` = (A `) \/ B
 B in bool E by Def1;
then A1: B c= E by ZFMISC_1:def_1;
thus (A \ B) ` = (E \ A) \/ (E /\ B) by XBOOLE_1:52
.= (A `) \/ B by A1, XBOOLE_1:28 ; ::_thesis: verum
end;

theorem :: SUBSET_1:15
for E being set
for A, B being Subset of E holds (A \+\ B) ` = (A /\ B) \/ ((A `) /\ (B `))
proof
let E be set ; ::_thesis: for A, B being Subset of E holds (A \+\ B) ` = (A /\ B) \/ ((A `) /\ (B `))
let A, B be Subset of E; ::_thesis: (A \+\ B) ` = (A /\ B) \/ ((A `) /\ (B `))
 A in bool E by Def1;
then A1: A c= E by ZFMISC_1:def_1;
thus (A \+\ B) ` = (E \ (A \/ B)) \/ ((E /\ A) /\ B) by XBOOLE_1:102
.= (A /\ B) \/ (E \ (A \/ B)) by A1, XBOOLE_1:28
.= (A /\ B) \/ ((A `) /\ (B `)) by XBOOLE_1:53 ; ::_thesis: verum
end;

theorem :: SUBSET_1:16
for E being set
for A, B being Subset of E st A c= B ` holds
B c= A `
proof
let E be set ; ::_thesis: for A, B being Subset of E st A c= B ` holds
B c= A `
let A, B be Subset of E; ::_thesis: ( A c= B ` implies B c= A ` )
assume  A c= B ` ; ::_thesis: B c= A `
then  (B `) ` c= A ` by Th12;
hence  B c= A ` ; ::_thesis: verum
end;

theorem :: SUBSET_1:17
for E being set
for A, B being Subset of E st A ` c= B holds
B ` c= A
proof
let E be set ; ::_thesis: for A, B being Subset of E st A ` c= B holds
B ` c= A
let A, B be Subset of E; ::_thesis: ( A ` c= B implies B ` c= A )
assume  A ` c= B ; ::_thesis: B ` c= A
then  B ` c= (A `) ` by Th12;
hence  B ` c= A ; ::_thesis: verum
end;

theorem :: SUBSET_1:18
for E being set
for A being Subset of E holds
( A c= A ` iff A = {} E )
proof
let E be set ; ::_thesis: for A being Subset of E holds
( A c= A ` iff A = {} E )
let A be Subset of E; ::_thesis: ( A c= A ` iff A = {} E )
thus  ( A c= A ` implies A = {} E ) by XBOOLE_1:38; ::_thesis: ( A = {} E implies A c= A ` )
 A in bool E by Def1;
hence  ( A = {} E implies A c= A ` ) by ZFMISC_1:def_1; ::_thesis: verum
end;

theorem :: SUBSET_1:19
for E being set
for A being Subset of E holds
( A ` c= A iff A = [#] E )
proof
let E be set ; ::_thesis: for A being Subset of E holds
( A ` c= A iff A = [#] E )
let A be Subset of E; ::_thesis: ( A ` c= A iff A = [#] E )
thus  ( A ` c= A implies A = [#] E ) ::_thesis: ( A = [#] E implies A ` c= A )
proof
assume  A ` c= A ; ::_thesis: A = [#] E
hence A = A \/ (A `) by XBOOLE_1:12
.= [#] E by Th10 ;
::_thesis: verum
end;
assume  A = [#] E ; ::_thesis: A ` c= A
then  A ` = {} by XBOOLE_1:37;
hence  A ` c= A by XBOOLE_1:2; ::_thesis: verum
end;

theorem :: SUBSET_1:20
for E, X being set
for A being Subset of E st X c= A & X c= A ` holds
X = {} by XBOOLE_1:67, XBOOLE_1:79;

theorem :: SUBSET_1:21
for E being set
for A, B being Subset of E holds (A \/ B) ` c= A `
proof
let E be set ; ::_thesis: for A, B being Subset of E holds (A \/ B) ` c= A `
let A, B be Subset of E; ::_thesis: (A \/ B) ` c= A `
 A c= A \/ B by XBOOLE_1:7;
hence  (A \/ B) ` c= A ` by Th12; ::_thesis: verum
end;

theorem :: SUBSET_1:22
for E being set
for A, B being Subset of E holds A ` c= (A /\ B) `
proof
let E be set ; ::_thesis: for A, B being Subset of E holds A ` c= (A /\ B) `
let A, B be Subset of E; ::_thesis: A ` c= (A /\ B) `
 A /\ B c= A by XBOOLE_1:17;
hence  A ` c= (A /\ B) ` by Th12; ::_thesis: verum
end;

theorem Th23: :: SUBSET_1:23
for E being set
for A, B being Subset of E holds
( A misses B iff A c= B ` )
proof
let E be set ; ::_thesis: for A, B being Subset of E holds
( A misses B iff A c= B ` )
let A, B be Subset of E; ::_thesis: ( A misses B iff A c= B ` )
thus  ( A misses B implies A c= B ` ) ::_thesis: ( A c= B ` implies A misses B )
proof
assume A1: A misses B ; ::_thesis: A c= B `
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B ` )
assume A2: x in A ; ::_thesis: x in B `
then A3: not x in B by A1, XBOOLE_0:3;
 x in E by A2, Lm1;
hence  x in B ` by A3, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A4: A c= B ` ; ::_thesis: A misses B
assume  A meets B ; ::_thesis: contradiction
then consider x being set  such that
A5: x in A and
A6: x in B by XBOOLE_0:3;
 x in E \ B by A4, A5, TARSKI:def_3;
hence  contradiction by A6, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem :: SUBSET_1:24
for E being set
for A, B being Subset of E holds
( A misses B ` iff A c= B )
proof
let E be set ; ::_thesis: for A, B being Subset of E holds
( A misses B ` iff A c= B )
let A, B be Subset of E; ::_thesis: ( A misses B ` iff A c= B )
 (B `) ` = B ;
hence  ( A misses B ` iff A c= B ) by Th23; ::_thesis: verum
end;

theorem :: SUBSET_1:25
for E being set
for A, B being Subset of E st A misses B & A ` misses B ` holds
A = B `
proof
let E be set ; ::_thesis: for A, B being Subset of E st A misses B & A ` misses B ` holds
A = B `
let A, B be Subset of E; ::_thesis: ( A misses B & A ` misses B ` implies A = B ` )
assume that
A1: A misses B and
A2: A ` misses B ` ; ::_thesis: A = B `
A3: A in bool E by Def1;
thus  A c= B ` :: according to XBOOLE_0:def_10 ::_thesis: B ` c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B ` )
assume A4: x in A ; ::_thesis: x in B `
then A5: not x in B by A1, XBOOLE_0:3;
 A c= E by A3, ZFMISC_1:def_1;
then  x in E by A4, TARSKI:def_3;
hence  x in B ` by A5, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B ` or x in A )
A6: ( x in A ` implies not x in B ` ) by A2, XBOOLE_0:3;
assume A7: x in B ` ; ::_thesis: x in A
then  x in E by XBOOLE_0:def_5;
hence  x in A by A7, A6, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem :: SUBSET_1:26
for E being set
for A, B, C being Subset of E st A c= B & C misses B holds
A c= C `
proof
let E be set ; ::_thesis: for A, B, C being Subset of E st A c= B & C misses B holds
A c= C `
let A, B, C be Subset of E; ::_thesis: ( A c= B & C misses B implies A c= C ` )
assume  ( A c= B & C misses B ) ; ::_thesis: A c= C `
then  A misses C by XBOOLE_1:63;
hence  A c= C ` by Th23; ::_thesis: verum
end;

theorem :: SUBSET_1:27
for E being set
for A, B being Subset of E st ( for a being Element of A holds a in B ) holds
A c= B
proof
let E be set ; ::_thesis: for A, B being Subset of E st ( for a being Element of A holds a in B ) holds
A c= B
let A, B be Subset of E; ::_thesis: ( ( for a being Element of A holds a in B ) implies A c= B )
assume A1: for a being Element of A holds a in B ; ::_thesis: A c= B
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in B )
assume  a in A ; ::_thesis: a in B
then  a is Element of A by Def1;
hence  a in B by A1; ::_thesis: verum
end;

theorem :: SUBSET_1:28
for E being set
for A being Subset of E st ( for x being Element of E holds x in A ) holds
E = A
proof
let E be set ; ::_thesis: for A being Subset of E st ( for x being Element of E holds x in A ) holds
E = A
let A be Subset of E; ::_thesis: ( ( for x being Element of E holds x in A ) implies E = A )
assume A1: for x being Element of E holds x in A ; ::_thesis: E = A
thus  E c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= E
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in E or a in A )
assume  a in E ; ::_thesis: a in A
then  a is Element of E by Def1;
hence  a in A by A1; ::_thesis: verum
end;
 A in bool E by Def1;
hence  A c= E by ZFMISC_1:def_1; ::_thesis: verum
end;

theorem :: SUBSET_1:29
for E being set st E <> {} holds
for B being Subset of E
for x being Element of E st not x in B holds
x in B `
proof
let E be set ; ::_thesis: ( E <> {} implies for B being Subset of E
for x being Element of E st not x in B holds
x in B ` )
assume A1: E <> {} ; ::_thesis: for B being Subset of E
for x being Element of E st not x in B holds
x in B `
let B be Subset of E; ::_thesis: for x being Element of E st not x in B holds
x in B `
let x be Element of E; ::_thesis: ( not x in B implies x in B ` )
assume A2: not x in B ; ::_thesis: x in B `
 x in E by A1, Def1;
hence  x in B ` by A2, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th30: :: SUBSET_1:30
for E being set
for A, B being Subset of E st ( for x being Element of E holds
( x in A iff not x in B ) ) holds
A = B `
proof
let E be set ; ::_thesis: for A, B being Subset of E st ( for x being Element of E holds
( x in A iff not x in B ) ) holds
A = B `
let A, B be Subset of E; ::_thesis: ( ( for x being Element of E holds
( x in A iff not x in B ) ) implies A = B ` )
assume A1: for x being Element of E holds
( x in A iff not x in B ) ; ::_thesis: A = B `
thus  A c= B ` :: according to XBOOLE_0:def_10 ::_thesis: B ` c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B ` )
assume A2: x in A ; ::_thesis: x in B `
 A in bool E by Def1;
then  A c= E by ZFMISC_1:def_1;
then  x in E by A2, TARSKI:def_3;
then  x is Element of E by Def1;
then A3: not x in B by A1, A2;
 x in E by A2, Lm1;
hence  x in B ` by A3, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B ` or x in A )
assume A4: x in B ` ; ::_thesis: x in A
 B ` in bool E by Def1;
then  B ` c= E by ZFMISC_1:def_1;
then  x in E by A4, TARSKI:def_3;
then reconsider x = x as Element of E by Def1;
 not x in B by A4, XBOOLE_0:def_5;
hence  x in A by A1; ::_thesis: verum
end;

theorem :: SUBSET_1:31
for E being set
for A, B being Subset of E st ( for x being Element of E holds
( not x in A iff x in B ) ) holds
A = B `
proof
let E be set ; ::_thesis: for A, B being Subset of E st ( for x being Element of E holds
( not x in A iff x in B ) ) holds
A = B `
let A, B be Subset of E; ::_thesis: ( ( for x being Element of E holds
( not x in A iff x in B ) ) implies A = B ` )
assume  for x being Element of E holds
( not x in A iff x in B ) ; ::_thesis: A = B `
then  for x being Element of E holds
( x in A iff not x in B ) ;
hence  A = B ` by Th30; ::_thesis: verum
end;

theorem :: SUBSET_1:32
for E being set
for A, B being Subset of E st ( for x being Element of E holds
( ( x in A & not x in B ) or ( x in B & not x in A ) ) ) holds
A = B `
proof
let E be set ; ::_thesis: for A, B being Subset of E st ( for x being Element of E holds
( ( x in A & not x in B ) or ( x in B & not x in A ) ) ) holds
A = B `
let A, B be Subset of E; ::_thesis: ( ( for x being Element of E holds
( ( x in A & not x in B ) or ( x in B & not x in A ) ) ) implies A = B ` )
assume  for x being Element of E holds
( ( x in A & not x in B ) or ( x in B & not x in A ) ) ; ::_thesis: A = B `
then  for x being Element of E holds
( x in A iff not x in B ) ;
hence  A = B ` by Th30; ::_thesis: verum
end;


theorem :: SUBSET_1:33
for X being set
for x1 being Element of X st X <> {} holds
{x1} is Subset of X
proof
let X be set ; ::_thesis: for x1 being Element of X st X <> {} holds
{x1} is Subset of X
let x1 be Element of X; ::_thesis: ( X <> {} implies {x1} is Subset of X )
assume  X <> {} ; ::_thesis: {x1} is Subset of X
then A1: x1 in X by Def1;
 {x1} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1} or x in X )
assume  x in {x1} ; ::_thesis: x in X
hence  x in X by A1, TARSKI:def_1; ::_thesis: verum
end;
then  {x1} in bool X by ZFMISC_1:def_1;
hence  {x1} is Subset of X by Def1; ::_thesis: verum
end;

theorem :: SUBSET_1:34
for X being set
for x1, x2 being Element of X st X <> {} holds
{x1,x2} is Subset of X
proof
let X be set ; ::_thesis: for x1, x2 being Element of X st X <> {} holds
{x1,x2} is Subset of X
let x1, x2 be Element of X; ::_thesis: ( X <> {} implies {x1,x2} is Subset of X )
assume  X <> {} ; ::_thesis: {x1,x2} is Subset of X
then A1: ( x1 in X & x2 in X ) by Def1;
 {x1,x2} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2} or x in X )
assume  x in {x1,x2} ; ::_thesis: x in X
hence  x in X by A1, TARSKI:def_2; ::_thesis: verum
end;
then  {x1,x2} in bool X by ZFMISC_1:def_1;
hence  {x1,x2} is Subset of X by Def1; ::_thesis: verum
end;

theorem :: SUBSET_1:35
for X being set
for x1, x2, x3 being Element of X st X <> {} holds
{x1,x2,x3} is Subset of X
proof
let X be set ; ::_thesis: for x1, x2, x3 being Element of X st X <> {} holds
{x1,x2,x3} is Subset of X
let x1, x2, x3 be Element of X; ::_thesis: ( X <> {} implies {x1,x2,x3} is Subset of X )
assume A1: X <> {} ; ::_thesis: {x1,x2,x3} is Subset of X
then A2: x3 in X by Def1;
A3: ( x1 in X & x2 in X ) by A1, Def1;
 {x1,x2,x3} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2,x3} or x in X )
assume  x in {x1,x2,x3} ; ::_thesis: x in X
hence  x in X by A3, A2, ENUMSET1:def_1; ::_thesis: verum
end;
then  {x1,x2,x3} in bool X by ZFMISC_1:def_1;
hence  {x1,x2,x3} is Subset of X by Def1; ::_thesis: verum
end;

theorem :: SUBSET_1:36
for X being set
for x1, x2, x3, x4 being Element of X st X <> {} holds
{x1,x2,x3,x4} is Subset of X
proof
let X be set ; ::_thesis: for x1, x2, x3, x4 being Element of X st X <> {} holds
{x1,x2,x3,x4} is Subset of X
let x1, x2, x3, x4 be Element of X; ::_thesis: ( X <> {} implies {x1,x2,x3,x4} is Subset of X )
assume A1: X <> {} ; ::_thesis: {x1,x2,x3,x4} is Subset of X
then A2: ( x3 in X & x4 in X ) by Def1;
A3: ( x1 in X & x2 in X ) by A1, Def1;
 {x1,x2,x3,x4} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2,x3,x4} or x in X )
assume  x in {x1,x2,x3,x4} ; ::_thesis: x in X
hence  x in X by A3, A2, ENUMSET1:def_2; ::_thesis: verum
end;
then  {x1,x2,x3,x4} in bool X by ZFMISC_1:def_1;
hence  {x1,x2,x3,x4} is Subset of X by Def1; ::_thesis: verum
end;

theorem :: SUBSET_1:37
for X being set
for x1, x2, x3, x4, x5 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5} is Subset of X
proof
let X be set ; ::_thesis: for x1, x2, x3, x4, x5 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5} is Subset of X
let x1, x2, x3, x4, x5 be Element of X; ::_thesis: ( X <> {} implies {x1,x2,x3,x4,x5} is Subset of X )
assume A1: X <> {} ; ::_thesis: {x1,x2,x3,x4,x5} is Subset of X
 {x1,x2,x3,x4,x5} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2,x3,x4,x5} or x in X )
A2: ( not x in {x1,x2,x3,x4,x5} or x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) by ENUMSET1:def_3;
assume  x in {x1,x2,x3,x4,x5} ; ::_thesis: x in X
hence  x in X by A1, A2, Def1; ::_thesis: verum
end;
then  {x1,x2,x3,x4,x5} in bool X by ZFMISC_1:def_1;
hence  {x1,x2,x3,x4,x5} is Subset of X by Def1; ::_thesis: verum
end;

theorem :: SUBSET_1:38
for X being set
for x1, x2, x3, x4, x5, x6 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6} is Subset of X
proof
let X be set ; ::_thesis: for x1, x2, x3, x4, x5, x6 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6} is Subset of X
let x1, x2, x3, x4, x5, x6 be Element of X; ::_thesis: ( X <> {} implies {x1,x2,x3,x4,x5,x6} is Subset of X )
assume A1: X <> {} ; ::_thesis: {x1,x2,x3,x4,x5,x6} is Subset of X
 {x1,x2,x3,x4,x5,x6} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2,x3,x4,x5,x6} or x in X )
A2: ( not x in {x1,x2,x3,x4,x5,x6} or x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) by ENUMSET1:def_4;
assume  x in {x1,x2,x3,x4,x5,x6} ; ::_thesis: x in X
hence  x in X by A1, A2, Def1; ::_thesis: verum
end;
then  {x1,x2,x3,x4,x5,x6} in bool X by ZFMISC_1:def_1;
hence  {x1,x2,x3,x4,x5,x6} is Subset of X by Def1; ::_thesis: verum
end;

theorem :: SUBSET_1:39
for X being set
for x1, x2, x3, x4, x5, x6, x7 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6,x7} is Subset of X
proof
let X be set ; ::_thesis: for x1, x2, x3, x4, x5, x6, x7 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6,x7} is Subset of X
let x1, x2, x3, x4, x5, x6, x7 be Element of X; ::_thesis: ( X <> {} implies {x1,x2,x3,x4,x5,x6,x7} is Subset of X )
assume A1: X <> {} ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7} is Subset of X
 {x1,x2,x3,x4,x5,x6,x7} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2,x3,x4,x5,x6,x7} or x in X )
A2: ( not x in {x1,x2,x3,x4,x5,x6,x7} or x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) by ENUMSET1:def_5;
assume  x in {x1,x2,x3,x4,x5,x6,x7} ; ::_thesis: x in X
hence  x in X by A1, A2, Def1; ::_thesis: verum
end;
then  {x1,x2,x3,x4,x5,x6,x7} in bool X by ZFMISC_1:def_1;
hence  {x1,x2,x3,x4,x5,x6,x7} is Subset of X by Def1; ::_thesis: verum
end;

theorem :: SUBSET_1:40
for X being set
for x1, x2, x3, x4, x5, x6, x7, x8 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X
proof
let X be set ; ::_thesis: for x1, x2, x3, x4, x5, x6, x7, x8 being Element of X st X <> {} holds
{x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X
let x1, x2, x3, x4, x5, x6, x7, x8 be Element of X; ::_thesis: ( X <> {} implies {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X )
assume A1: X <> {} ; ::_thesis: {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X
 {x1,x2,x3,x4,x5,x6,x7,x8} c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2,x3,x4,x5,x6,x7,x8} or x in X )
A2: ( not x in {x1,x2,x3,x4,x5,x6,x7,x8} or x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) by ENUMSET1:def_6;
assume  x in {x1,x2,x3,x4,x5,x6,x7,x8} ; ::_thesis: x in X
hence  x in X by A1, A2, Def1; ::_thesis: verum
end;
then  {x1,x2,x3,x4,x5,x6,x7,x8} in bool X by ZFMISC_1:def_1;
hence  {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X by Def1; ::_thesis: verum
end;

theorem :: SUBSET_1:41
for x, X being set st x in X holds
{x} is Subset of X
proof
let x, X be set ; ::_thesis: ( x in X implies {x} is Subset of X )
assume  x in X ; ::_thesis: {x} is Subset of X
then  {x} c= X by ZFMISC_1:31;
then  {x} in bool X by ZFMISC_1:def_1;
hence  {x} is Subset of X by Def1; ::_thesis: verum
end;

scheme :: SUBSET_1:sch 1
SubsetEx{ F1() ->  set , P1[ set ] } :
 ex X being Subset of F1() st
for x being set holds
( x in X iff ( x in F1() & P1[x] ) )
proof
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in F1() & P1[x] ) ) from XBOOLE_0:sch_1();
 X c= F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in F1() )
thus  ( not x in X or x in F1() ) by A1; ::_thesis: verum
end;
then  X in bool F1() by ZFMISC_1:def_1;
then reconsider X = X as Subset of F1() by Def1;
take  X ; ::_thesis: for x being set holds
( x in X iff ( x in F1() & P1[x] ) )
thus  for x being set holds
( x in X iff ( x in F1() & P1[x] ) ) by A1; ::_thesis: verum
end;

scheme :: SUBSET_1:sch 2
SubsetEq{ F1() ->  set , F2() ->  Subset of F1(), F3() ->  Subset of F1(), P1[ set ] } :
 F2() = F3()
provided
A1: for y being Element of F1() holds
( y in F2() iff P1[y] ) and
A2: for y being Element of F1() holds
( y in F3() iff P1[y] )
proof
 for x being Element of F1() holds
( x in F2() iff x in F3() )
proof
let x be Element of F1(); ::_thesis: ( x in F2() iff x in F3() )
hereby  ::_thesis: ( x in F3() implies x in F2() )
assume  x in F2() ; ::_thesis: x in F3()
then  P1[x] by A1;
hence  x in F3() by A2; ::_thesis: verum
end;
assume  x in F3() ; ::_thesis: x in F2()
then  P1[x] by A2;
hence  x in F2() by A1; ::_thesis: verum
end;
hence  F2() = F3() by Th3; ::_thesis: verum
end;

definition
let X, Y be non empty set ;
:: original: misses
redefine predX misses Y;
irreflexivity
 for X being non empty set holds R5(b1,b1)
proof
let A be non empty set ; ::_thesis: R5(A,A)
 ex x being set st x in A by XBOOLE_0:def_1;
hence  R5(A,A) by XBOOLE_0:3; ::_thesis: verum
end;
end;

definition
let X, Y be non empty set ;
:: original: misses
redefine predX meets Y;
reflexivity
 for X being non empty set holds R5(b1,b1)
proof
let A be non empty set ; ::_thesis: R5(A,A)
thus  not A misses A ; ::_thesis: verum
end;
end;

definition
let S be set ;
func choose S ->  Element of S equals :: SUBSET_1:def 5
 the Element of S;
correctness
coherence
the Element of S is Element of S;
;
end;

:: deftheorem  defines choose SUBSET_1:def_5_:_
 for S being set holds choose S = the Element of S;

begin

 Lm2:  for X, Y being set st ( for x being set st x in X holds
x in Y ) holds
X is Subset of Y
proof
let X, Y be set ; ::_thesis: ( ( for x being set st x in X holds
x in Y ) implies X is Subset of Y )
assume  for x being set st x in X holds
x in Y ; ::_thesis: X is Subset of Y
then  X c= Y by TARSKI:def_3;
then  X in bool Y by ZFMISC_1:def_1;
hence  X is Subset of Y by Def1; ::_thesis: verum
end;

Lm3:  for x, E being set
for A being Subset of E st x in A holds
x is Element of E
proof
let x, E be set ; ::_thesis: for A being Subset of E st x in A holds
x is Element of E
let A be Subset of E; ::_thesis: ( x in A implies x is Element of E )
assume  x in A ; ::_thesis: x is Element of E
then  x in E by Lm1;
hence  x is Element of E by Def1; ::_thesis: verum
end;

scheme :: SUBSET_1:sch 3
SubsetEx{ F1() ->  non empty set , P1[ set ] } :
 ex B being Subset of F1() st
for x being Element of F1() holds
( x in B iff P1[x] )
proof
consider B being set  such that
A1: for x being set holds
( x in B iff ( x in F1() & P1[x] ) ) from XBOOLE_0:sch_1();
 for x being set st x in B holds
x in F1() by A1;
then reconsider B = B as Subset of F1() by Lm2;
take  B ; ::_thesis: for x being Element of F1() holds
( x in B iff P1[x] )
let x be Element of F1(); ::_thesis: ( x in B iff P1[x] )
 x in F1() by Def1;
hence  ( x in B iff P1[x] ) by A1; ::_thesis: verum
end;

scheme :: SUBSET_1:sch 4
SubComp{ F1() ->  set , F2() ->  Subset of F1(), F3() ->  Subset of F1(), P1[ set ] } :
 F2() = F3()
provided
A1: for X being Element of F1() holds
( X in F2() iff P1[X] ) and
A2: for X being Element of F1() holds
( X in F3() iff P1[X] )
proof
thus  F2() c= F3() :: according to XBOOLE_0:def_10 ::_thesis: F3() c= F2()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F2() or x in F3() )
assume A3: x in F2() ; ::_thesis: x in F3()
then reconsider X = x as Element of F1() by Lm3;
 P1[X] by A1, A3;
hence  x in F3() by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F3() or x in F2() )
assume A4: x in F3() ; ::_thesis: x in F2()
then reconsider X = x as Element of F1() by Lm3;
 P1[X] by A2, A4;
hence  x in F2() by A1; ::_thesis: verum
end;

theorem :: SUBSET_1:42
for E being set
for A, B being Subset of E st A ` = B ` holds
A = B
proof
let E be set ; ::_thesis: for A, B being Subset of E st A ` = B ` holds
A = B
let A, B be Subset of E; ::_thesis: ( A ` = B ` implies A = B )
assume  A ` = B ` ; ::_thesis: A = B
hence A = (B `) `
.= B ;
::_thesis: verum
end;

registration
let X be empty set ;
cluster  ->  empty for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is empty
proof
let Y be Subset of X; ::_thesis: Y is empty
 Y in bool X by Def1;
then  Y c= X by ZFMISC_1:def_1;
hence  Y is empty by XBOOLE_1:3; ::_thesis: verum
end;
end;

definition
let E be set ;
let A be Subset of E;
attrA is proper  means :: SUBSET_1:def 6
A <> E;
end;

:: deftheorem  defines proper SUBSET_1:def_6_:_
 for E being set
for A being Subset of E holds
( A is proper iff A <> E );

registration
let E be set ;
cluster [#] E ->  non proper ;
coherence
 not [#] E is proper
proof
thus  [#] E = E ; :: according to SUBSET_1:def_6 ::_thesis: verum
end;
end;

registration
let E be set ;
cluster non proper for Element of bool E;
existence
 not for b1 being Subset of E holds b1 is proper
proof
take  [#] E ; ::_thesis: not [#] E is proper
thus  not [#] E is proper ; ::_thesis: verum
end;
end;

registration
let E be non empty set ;
cluster non proper  ->  non empty for Element of bool E;
coherence
 for b1 being Subset of E st not b1 is proper holds
not b1 is empty
proof
let A be Subset of E; ::_thesis: ( not A is proper implies not A is empty )
assume  A = E ; :: according to SUBSET_1:def_6 ::_thesis: not A is empty
hence  not A is empty ; ::_thesis: verum
end;
cluster empty  ->  proper for Element of bool E;
coherence
 for b1 being Subset of E st b1 is empty holds
b1 is proper ;
end;

registration
let E be non empty set ;
cluster proper for Element of bool E;
existence
 ex b1 being Subset of E st b1 is proper
proof
take  {} E ; ::_thesis: {} E is proper
thus  {} E <> E ; :: according to SUBSET_1:def_6 ::_thesis: verum
end;
end;

registration
let E be empty set ;
cluster  ->  non proper for Element of bool E;
coherence
 for b1 being Subset of E holds not b1 is proper
proof
let A be Subset of E; ::_thesis: not A is proper
thus  A = E ; :: according to SUBSET_1:def_6 ::_thesis: verum
end;
end;

theorem :: SUBSET_1:43
for X, Y, A, z being set st z in A & A c= [:X,Y:] holds
ex x being Element of X ex y being Element of Y st z = [x,y]
proof
let X, Y, A be set ; ::_thesis: for z being set st z in A & A c= [:X,Y:] holds
ex x being Element of X ex y being Element of Y st z = [x,y]
let z be set ; ::_thesis: ( z in A & A c= [:X,Y:] implies ex x being Element of X ex y being Element of Y st z = [x,y] )
assume  ( z in A & A c= [:X,Y:] ) ; ::_thesis: ex x being Element of X ex y being Element of Y st z = [x,y]
then consider x, y being set  such that
A1: x in X and
A2: y in Y and
A3: z = [x,y] by ZFMISC_1:84;
reconsider y = y as Element of Y by A2, Def1;
reconsider x = x as Element of X by A1, Def1;
take  x ; ::_thesis: ex y being Element of Y st z = [x,y]
take  y ; ::_thesis: z = [x,y]
thus  z = [x,y] by A3; ::_thesis: verum
end;

theorem :: SUBSET_1:44
for X being non empty set
for A, B being non empty Subset of X st A c< B holds
ex p being Element of X st
( p in B & A c= B \ {p} )
proof
let X be non empty set ; ::_thesis: for A, B being non empty Subset of X st A c< B holds
ex p being Element of X st
( p in B & A c= B \ {p} )
let A, B be non empty Subset of X; ::_thesis: ( A c< B implies ex p being Element of X st
( p in B & A c= B \ {p} ) )
assume A1: A c< B ; ::_thesis: ex p being Element of X st
( p in B & A c= B \ {p} )
then consider p being Element of X such that
A2: p in B \ A by Th4, XBOOLE_1:105;
A3: not p in A by A2, XBOOLE_0:def_5;
take  p ; ::_thesis: ( p in B & A c= B \ {p} )
 A c= B by A1, XBOOLE_0:def_8;
hence  ( p in B & A c= B \ {p} ) by A2, A3, XBOOLE_0:def_5, ZFMISC_1:34; ::_thesis: verum
end;

definition
let X be non empty set ;
redefine attr X is trivial  means :: SUBSET_1:def 7
 for x, y being Element of X holds x = y;
compatibility
 ( X is trivial iff for x, y being Element of X holds x = y )
proof
thus  ( X is trivial implies for x, y being Element of X holds x = y ) ::_thesis: ( ( for x, y being Element of X holds x = y ) implies X is trivial )
proof
assume A1: X is trivial ; ::_thesis: for x, y being Element of X holds x = y
let x, y be Element of X; ::_thesis: x = y
 ( x in X & y in X ) by Def1;
hence  x = y by A1, ZFMISC_1:def_10; ::_thesis: verum
end;
assume A2: for x, y being Element of X holds x = y ; ::_thesis: X is trivial
let x, y be set ; :: according to ZFMISC_1:def_10 ::_thesis: ( not x in X or not y in X or x = y )
assume  ( x in X & y in X ) ; ::_thesis: x = y
then  ( x is Element of X & y is Element of X ) by Def1;
hence  x = y by A2; ::_thesis: verum
end;
end;

:: deftheorem  defines trivial SUBSET_1:def_7_:_
 for X being non empty set holds
( X is trivial iff for x, y being Element of X holds x = y );

registration
let X be non empty set ;
cluster non empty trivial for Element of bool X;
existence
 ex b1 being Subset of X st
( not b1 is empty & b1 is trivial )
proof
 the Element of X in X by Def1;
then  { the Element of X} c= X by ZFMISC_1:31;
then  { the Element of X} in bool X by ZFMISC_1:def_1;
then reconsider A = { the Element of X} as Subset of X by Def1;
take  A ; ::_thesis: ( not A is empty & A is trivial )
thus  not A is empty ; ::_thesis: A is trivial
let x, y be set ; :: according to ZFMISC_1:def_10 ::_thesis: ( not x in A or not y in A or x = y )
assume  ( x in A & y in A ) ; ::_thesis: x = y
then  ( x = the Element of X & y = the Element of X ) by TARSKI:def_1;
hence  x = y ; ::_thesis: verum
end;
end;

registration
let X be trivial set ;
cluster  ->  trivial for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is trivial
proof
let Y be Subset of X; ::_thesis: Y is trivial
let x, y be set ; :: according to ZFMISC_1:def_10 ::_thesis: ( not x in Y or not y in Y or x = y )
assume  ( x in Y & y in Y ) ; ::_thesis: x = y
then  ( x in X & y in X ) by Lm1;
hence  x = y by ZFMISC_1:def_10; ::_thesis: verum
end;
end;

registration
let X be non trivial set ;
cluster non trivial for Element of bool X;
existence
 not for b1 being Subset of X holds b1 is trivial
proof
take  [#] X ; ::_thesis: not [#] X is trivial
thus  not [#] X is trivial ; ::_thesis: verum
end;
end;

theorem :: SUBSET_1:45
for D being set
for A being Subset of D st not A is trivial holds
ex d1, d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 )
proof
let D be set ; ::_thesis: for A being Subset of D st not A is trivial holds
ex d1, d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 )
let A be Subset of D; ::_thesis: ( not A is trivial implies ex d1, d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 ) )
assume  not A is trivial ; ::_thesis: ex d1, d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 )
then consider d1, d2 being set  such that
A1: ( d1 in A & d2 in A ) and
A2: d1 <> d2 by ZFMISC_1:def_10;
 ( d1 in D & d2 in D ) by A1, Lm1;
then reconsider d1 = d1, d2 = d2 as Element of D by Def1;
take  d1 ; ::_thesis: ex d2 being Element of D st
( d1 in A & d2 in A & d1 <> d2 )
take  d2 ; ::_thesis: ( d1 in A & d2 in A & d1 <> d2 )
thus  ( d1 in A & d2 in A & d1 <> d2 ) by A1, A2; ::_thesis: verum
end;

theorem Th46: :: SUBSET_1:46
for X being non empty trivial set ex x being Element of X st X = {x}
proof
let X be non empty trivial set ; ::_thesis: ex x being Element of X st X = {x}
consider x being set  such that
A1: X = {x} by ZFMISC_1:131;
 x in X by A1, TARSKI:def_1;
then reconsider x = x as Element of X by Def1;
take  x ; ::_thesis: X = {x}
thus  X = {x} by A1; ::_thesis: verum
end;

theorem :: SUBSET_1:47
for X being non empty set
for A being non empty Subset of X st A is trivial holds
ex x being Element of X st A = {x}
proof
let X be non empty set ; ::_thesis: for A being non empty Subset of X st A is trivial holds
ex x being Element of X st A = {x}
let A be non empty Subset of X; ::_thesis: ( A is trivial implies ex x being Element of X st A = {x} )
assume  A is trivial ; ::_thesis: ex x being Element of X st A = {x}
then  ex s being Element of A st A = {s} by Th46;
hence  ex x being Element of X st A = {x} ; ::_thesis: verum
end;

theorem :: SUBSET_1:48
for X being non trivial set
for x being Element of X ex y being set st
( y in X & x <> y )
proof
let X be non trivial set ; ::_thesis: for x being Element of X ex y being set st
( y in X & x <> y )
let x be Element of X; ::_thesis: ex y being set st
( y in X & x <> y )
consider d1, d2 being set  such that
A1: ( d1 in X & d2 in X ) and
A2: d1 <> d2 by ZFMISC_1:def_10;
 ( x <> d1 or x <> d2 ) by A2;
hence  ex y being set st
( y in X & x <> y ) by A1; ::_thesis: verum
end;