:: FINSUB_1 semantic presentation

begin

definition
let IT be ( ( ) ( ) set ) ;
attr IT is cup-closed means :: FINSUB_1:def 1
 for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) in IT : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) in IT : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) in IT : ( ( ) ( ) set ) ;
attr IT is cap-closed means :: FINSUB_1:def 2
 for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) in IT : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) in IT : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) in IT : ( ( ) ( ) set ) ;
attr IT is diff-closed means :: FINSUB_1:def 3
 for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) in IT : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) in IT : ( ( ) ( ) set ) holds
X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) in IT : ( ( ) ( ) set ) ;
end;

definition
let IT be ( ( ) ( ) set ) ;
attr IT is preBoolean means :: FINSUB_1:def 4
( IT : ( ( ) ( ) set ) is cup-closed & IT : ( ( ) ( ) set ) is diff-closed );
end;

registration
cluster preBoolean -> cup-closed diff-closed for ( ( ) ( ) set ) ;
cluster cup-closed diff-closed -> preBoolean for ( ( ) ( ) set ) ;
end;

registration
cluster non empty cup-closed cap-closed diff-closed for ( ( ) ( ) set ) ;
end;

theorem :: FINSUB_1:1
for A being ( ( ) ( ) set ) holds
( A : ( ( ) ( ) set ) is preBoolean iff for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) & Y : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) holds
( X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) & X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) set ) ) ) ;

definition
let A be ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ;
let X, Y be ( ( ) ( ) Element of A : ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;
:: original: \/
redefine func X \/ Y -> ( ( ) ( ) Element of A : ( ( non trivial ) ( non trivial ) set ) ) ;
:: original: \
redefine func X \ Y -> ( ( ) ( ) Element of A : ( ( non trivial ) ( non trivial ) set ) ) ;
end;

theorem :: FINSUB_1:2
for X, Y being ( ( ) ( ) set )
for A being ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) st X : ( ( ) ( ) set ) is ( ( ) ( ) Element of A : ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & Y : ( ( ) ( ) set ) is ( ( ) ( ) Element of A : ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds
X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( ) ( ) Element of A : ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: FINSUB_1:3
for X, Y being ( ( ) ( ) set )
for A being ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) st X : ( ( ) ( ) set ) is ( ( ) ( ) Element of A : ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & Y : ( ( ) ( ) set ) is ( ( ) ( ) Element of A : ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds
X : ( ( ) ( ) set ) \+\ Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( ) ( ) Element of A : ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: FINSUB_1:4
for A being ( ( non empty ) ( non empty ) set ) st ( for X, Y being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) holds
( X : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) \+\ Y : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in A : ( ( non empty ) ( non empty ) set ) & X : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) \ Y : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) in A : ( ( non empty ) ( non empty ) set ) ) ) holds
A : ( ( non empty ) ( non empty ) set ) is preBoolean ;

theorem :: FINSUB_1:5
for A being ( ( non empty ) ( non empty ) set ) st ( for X, Y being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) holds
( X : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) \+\ Y : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in A : ( ( non empty ) ( non empty ) set ) & X : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) /\ Y : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in A : ( ( non empty ) ( non empty ) set ) ) ) holds
A : ( ( non empty ) ( non empty ) set ) is preBoolean ;

theorem :: FINSUB_1:6
for A being ( ( non empty ) ( non empty ) set ) st ( for X, Y being ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) holds
( X : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) \+\ Y : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in A : ( ( non empty ) ( non empty ) set ) & X : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) \/ Y : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) in A : ( ( non empty ) ( non empty ) set ) ) ) holds
A : ( ( non empty ) ( non empty ) set ) is preBoolean ;

definition
let A be ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ;
let X, Y be ( ( ) ( ) Element of A : ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;
:: original: /\
redefine func X /\ Y -> ( ( ) ( ) Element of A : ( ( non trivial ) ( non trivial ) set ) ) ;
:: original: \+\
redefine func X \+\ Y -> ( ( ) ( ) Element of A : ( ( non trivial ) ( non trivial ) set ) ) ;
end;

theorem :: FINSUB_1:7
for A being ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) holds {} : ( ( ) ( empty finite V18() ) set ) in A : ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ;

theorem :: FINSUB_1:8
for A being ( ( ) ( ) set ) holds bool A : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) is preBoolean ;

registration
let A be ( ( ) ( ) set ) ;
cluster bool A : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) -> preBoolean ;
end;

theorem :: FINSUB_1:9
for A, B being ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) holds
( not A : ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) /\ B : ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( ) set ) is empty & A : ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) /\ B : ( ( non empty preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( ) set ) is preBoolean ) ;

definition
let A be ( ( ) ( ) set ) ;
func Fin A -> ( ( preBoolean ) ( cup-closed diff-closed preBoolean ) set ) means :: FINSUB_1:def 5
 for X being ( ( ) ( ) set ) holds
( X : ( ( ) ( ) set ) in it : ( ( non empty ) ( non empty ) set ) iff ( X : ( ( ) ( ) set ) c= A : ( ( non trivial ) ( non trivial ) set ) & X : ( ( ) ( ) set ) is finite ) );
end;

registration
let A be ( ( ) ( ) set ) ;
cluster Fin A : ( ( ) ( ) set ) : ( ( preBoolean ) ( cup-closed diff-closed preBoolean ) set ) -> non empty preBoolean ;
end;

registration
let A be ( ( ) ( ) set ) ;
cluster -> finite for ( ( ) ( ) Element of Fin A : ( ( non trivial ) ( non trivial ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;
end;

theorem :: FINSUB_1:10
for A, B being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) c= B : ( ( ) ( ) set ) holds
Fin A : ( ( ) ( ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) c= Fin B : ( ( ) ( ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ;

theorem :: FINSUB_1:11
for A, B being ( ( ) ( ) set ) holds Fin (A : ( ( ) ( ) set ) /\ B : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) = (Fin A : ( ( ) ( ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) /\ (Fin B : ( ( ) ( ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( ) set ) ;

theorem :: FINSUB_1:12
for A, B being ( ( ) ( ) set ) holds (Fin A : ( ( ) ( ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) \/ (Fin B : ( ( ) ( ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( non empty ) set ) c= Fin (A : ( ( ) ( ) set ) \/ B : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ;

theorem :: FINSUB_1:13
for A being ( ( ) ( ) set ) holds Fin A : ( ( ) ( ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) c= bool A : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ;

theorem :: FINSUB_1:14
for A being ( ( ) ( ) set ) st A : ( ( ) ( ) set ) is finite holds
Fin A : ( ( ) ( ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) = bool A : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ;

theorem :: FINSUB_1:15
Fin {} : ( ( ) ( empty finite V18() ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) = {{} : ( ( ) ( empty finite V18() ) set ) } : ( ( ) ( non empty finite V18() ) set ) ;

definition
let A be ( ( ) ( ) set ) ;
mode Finite_Subset of A is ( ( ) ( finite ) Element of Fin A : ( ( non trivial ) ( non trivial ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;
end;

theorem :: FINSUB_1:16
for A being ( ( ) ( ) set )
for X being ( ( ) ( finite ) Finite_Subset of A : ( ( ) ( ) set ) ) holds X : ( ( ) ( finite ) Finite_Subset of b1 : ( ( ) ( ) set ) ) is finite ;

theorem :: FINSUB_1:17
for A being ( ( ) ( ) set )
for X being ( ( ) ( finite ) Finite_Subset of A : ( ( ) ( ) set ) ) holds X : ( ( ) ( finite ) Finite_Subset of b1 : ( ( ) ( ) set ) ) is ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: FINSUB_1:18
for A being ( ( ) ( ) set )
for X being ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) st A : ( ( ) ( ) set ) is finite holds
X : ( ( ) ( ) Subset of ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) is ( ( ) ( finite ) Finite_Subset of A : ( ( ) ( ) set ) ) ;