:: BAGORDER semantic presentation

theorem Th1: :: BAGORDER:1
for b1, b2, b3 being set holds
( b3 in b1 & b3 in b2 implies ( b1 \ {b3} = b2 \ {b3} iff b1 = b2 ) )
proof
let c1, c2, c3 be set ;
assume E2: ( c3 in c1 & c3 in c2 ) ;
hereby
assume E3: c1 \ {c3} = c2 \ {c3} ;
thus c1 = c1 \/ {c3} by E2, ZFMISC_1:46
.= (c2 \ {c3}) \/ {c3} by E3, XBOOLE_1:39
.= c2 \/ {c3} by XBOOLE_1:39
.= c2 by E2, ZFMISC_1:46 ;
end;
thus ( c1 = c2 implies c1 \ {c3} = c2 \ {c3} ) ;
end;

theorem Th2: :: BAGORDER:2
for b1, b2 being Nat holds
( b2 in Seg b1 iff ( b2 - 1 is Nat & b2 - 1 < b1 ) )
proof
let c1, c2 be Nat;
E2: Seg c1 = { b1 where B is Nat : ( 1 <= b1 & b1 <= c1 ) } by FINSEQ_1:def 1;
hereby
assume c2 in Seg c1 ;
then consider c3 being Nat such that
E3: ( c2 = c3 & 1 <= c3 & c3 <= c1 ) by E2;
set c4 = c2 - 1;
set c5 = c1 - 1;
0 < c3 by E3;
then reconsider c6 = c2 - 1 as Nat by E3, NAT_1:60;
c6 = c2 - 1 ;
hence c2 - 1 is Nat ;
0 < c1 by E3;
then reconsider c7 = c1 - 1 as Nat by NAT_1:60;
c2 + (- 1) <= c1 + (- 1) by E3, XREAL_1:8;
then c6 <= c7 ;
then c2 - 1 < c7 + 1 by NAT_1:38;
hence c2 - 1 < c1 ;
end;
assume E3: ( c2 - 1 is Nat & c2 - 1 < c1 ) ;
then reconsider c3 = c2 - 1 as Nat ;
0 <= c3 ;
then E4: 0 + 1 <= (c2 - 1) + 1 by XREAL_1:8;
reconsider c4 = c1 - 1 as Nat by E3, NAT_1:60;
(c2 - 1) + 1 <= (c1 - 1) + 1 by E3, NAT_1:38;
hence c2 in Seg c1 by E2, E4;
end;

registration
let c1 be natural-yielding Function;
let c2 be set ;
cluster a1 | a2 -> natural-yielding ;
coherence
c1 | c2 is natural-yielding
proof
E2: rng c1 c= NAT by SEQM_3:def 8;
rng (c1 | c2) c= rng c1 by RELAT_1:99;
then rng (c1 | c2) c= NAT by E2, XBOOLE_1:1;
hence c1 | c2 is natural-yielding by SEQM_3:def 8;
end;
end;

registration
let c1 be finite-support Function;
let c2 be set ;
cluster a1 | a2 -> finite-support ;
coherence
c1 | c2 is finite-support
proof
support (c1 | c2) c= support c1
proof
let c3 be set ; :: according to TARSKI:def 3
assume E2: c3 in support (c1 | c2) ;
then E3: (c1 | c2) . c3 <> 0 by POLYNOM1:def 7;
support (c1 | c2) c= dom (c1 | c2) by POLYNOM1:41;
then c1 . c3 <> 0 by E2, E3, FUNCT_1:70;
hence c3 in support c1 by POLYNOM1:def 7;
end;
then support (c1 | c2) is finite by FINSET_1:13;
hence c1 | c2 is finite-support by POLYNOM1:def 8;
end;
end;

theorem Th3: :: BAGORDER:3
for b1 being Function
for b2 being set holds
( b2 in dom b1 implies b1 * <*b2*> = <*(b1 . b2)*> )
proof
let c1 be Function;
let c2 be set ;
assume E3: c2 in dom c1 ;
then c1 . c2 in rng c1 by FUNCT_1:def 5;
then reconsider c3 = dom c1, c4 = rng c1 as non empty set by E3;
reconsider c5 = c1 as Function of c3,c4 by FUNCT_2:def 1, RELSET_1:11;
rng <*c2*> = {c2} by FINSEQ_1:55;
then rng <*c2*> c= c3 by E3, ZFMISC_1:37;
then reconsider c6 = <*c2*> as FinSequence of c3 by FINSEQ_1:def 4;
thus c1 * <*c2*> = c5 * c6
.= <*(c1 . c2)*> by FINSEQ_2:39 ;
end;

theorem Th4: :: BAGORDER:4
for b1, b2, b3 being Function holds
( dom b1 = dom b2 & rng b1 c= dom b3 & rng b2 c= dom b3 & b1,b2 are_fiberwise_equipotent implies b3 * b1,b3 * b2 are_fiberwise_equipotent )
proof
let c1, c2, c3 be Function;
assume that
E4: dom c1 = dom c2 and
E5: rng c1 c= dom c3 and
E6: rng c2 c= dom c3 and
E7: c1,c2 are_fiberwise_equipotent ;
consider c4 being Permutation of dom c1 such that
E8: c1 = c2 * c4 by E4, E7, RFINSEQ:6;
E9: dom (c3 * c1) = dom c1 by E5, RELAT_1:46;
E10: dom (c3 * c2) = dom c2 by E6, RELAT_1:46;
c3 * c1 = (c3 * c2) * c4 by E8, RELAT_1:55;
hence c3 * c1,c3 * c2 are_fiberwise_equipotent by E4, E9, E10, RFINSEQ:6;
end;

theorem Th5: :: BAGORDER:5
for b1 being FinSequence of NAT holds
( Sum b1 = 0 iff b1 = (len b1) |-> 0 )
proof
let c1 be FinSequence of NAT ;
rng c1 c= NAT by FINSEQ_1:def 4;
then rng c1 c= REAL by XBOOLE_1:1;
then reconsider c2 = c1 as FinSequence of REAL by FINSEQ_1:def 4;
hereby
assume E5: Sum c1 = 0 ;
E6: Seg (len c1) = dom c1 by FINSEQ_1:def 3;
E7: Seg (len c1) = dom ((len c1) |-> 0) by FUNCOP_1:19;
now
let c3 be Nat;
assume E8: c3 in Seg (len c1) ;
now
assume c1 . c3 <> 0 ;
then 0 < c1 . c3 ;
then E9: ex b1 being Nat st
( b1 in dom c2 & 0 < c1 . b1 ) by E6, E8;
for b1 being Nat holds
( b1 in dom c1 implies 0 <= c1 . b1 ) ;
hence not verum by E5, E9, RVSUM_1:115;
end;
hence c1 . c3 = ((len c1) |-> 0) . c3 by E8, FUNCOP_1:13;
end;
hence c1 = (len c1) |-> 0 by E6, E7, FINSEQ_1:17;
end;
assume c1 = (len c1) |-> 0 ;
hence Sum c1 = 0 by RVSUM_1:111;
end;

definition
let c1, c2, c3 be Nat;
let c4 be ManySortedSet of c1;
func c2,c3 -cut c4 -> ManySortedSet of a3 -' a2 means :Def1: :: BAGORDER:def 1
for b1 being Nat holds
( b1 in a3 -' a2 implies a5 . b1 = a4 . (a2 + b1) );
existence
ex b1 being ManySortedSet of c3 -' c2 st
for b2 being Nat holds
( b2 in c3 -' c2 implies b1 . b2 = c4 . (c2 + b2) )
proof
defpred S1[ set , set ] means ex b1 being Nat st
( b1 = a1 & a2 = c4 . (c2 + b1) );
E5: for b1, b2, b3 being set holds
( b1 in c3 -' c2 & S1[b1,b2] & S1[b1,b3] implies b2 = b3 ) ;
now
let c5 be set ;
assume E6: c5 in c3 -' c2 ;
c3 -' c2 = { b1 where B is Nat : b1 < c3 -' c2 } by AXIOMS:30;
then consider c6 being Nat such that
E7: ( c5 = c6 & c6 < c3 -' c2 ) by E6;
reconsider c7 = c5 as Nat by E7;
consider c8 being set such that
E8: c8 = c4 . (c2 + c7) ;
take c9 = c8;
thus S1[c5,c9] by E8;
end;
then E6: for b1 being set holds
not ( b1 in c3 -' c2 & ( for b2 being set holds
not S1[b1,b2] ) ) ;
consider c5 being Function such that
E7: dom c5 = c3 -' c2 and
E8: for b1 being set holds
( b1 in c3 -' c2 implies S1[b1,c5 . b1] ) from FUNCT_1:sch 2(E5, E6);
 reconsider c6 = c5 as ManySortedSet of c3 -' c2 by E7, PBOOLE:def 3;
take c6 ;
let c7 be Nat;
assume E9: c7 in c3 -' c2 ;
consider c8 being Nat such that
E10: ( c8 = c7 & c6 . c7 = c4 . (c2 + c8) ) by E8, E9;
thus c6 . c7 = c4 . (c2 + c7) by E10;
end;
uniqueness
for b1, b2 being ManySortedSet of c3 -' c2 holds
( ( for b3 being Nat holds
( b3 in c3 -' c2 implies b1 . b3 = c4 . (c2 + b3) ) ) & ( for b3 being Nat holds
( b3 in c3 -' c2 implies b2 . b3 = c4 . (c2 + b3) ) ) implies b1 = b2 )
proof
let c5, c6 be ManySortedSet of c3 -' c2;
assume that
E5: for b1 being Nat holds
( b1 in c3 -' c2 implies c5 . b1 = c4 . (c2 + b1) ) and
E6: for b1 being Nat holds
( b1 in c3 -' c2 implies c6 . b1 = c4 . (c2 + b1) ) ;
E7: ( c3 -' c2 = dom c5 & c3 -' c2 = dom c6 ) by PBOOLE:def 3;
now
let c7 be set ;
assume E8: c7 in c3 -' c2 ;
c3 -' c2 = { b1 where B is Nat : b1 < c3 -' c2 } by AXIOMS:30;
then consider c8 being Nat such that
E9: ( c7 = c8 & c8 < c3 -' c2 ) by E8;
reconsider c9 = c7 as Nat by E9;
c5 . c7 = c4 . (c2 + c9) by E5, E8;
hence c5 . c7 = c6 . c7 by E6, E8;
end;
hence c5 = c6 by E7, FUNCT_1:9;
end;
end;

:: deftheorem Def1 defines -cut BAGORDER:def 1 :
for b1, b2, b3 being Nat
for b4 being ManySortedSet of b1
for b5 being ManySortedSet of b3 -' b2 holds
( b5 = b2,b3 -cut b4 iff for b6 being Nat holds
( b6 in b3 -' b2 implies b5 . b6 = b4 . (b2 + b6) ) );

registration
let c1, c2, c3 be Nat;
let c4 be natural-yielding ManySortedSet of c1;
cluster a2,a3 -cut a4 -> natural-yielding ;
coherence
c2,c3 -cut c4 is natural-yielding
proof
now
let c5 be set ;
assume E6: c5 in rng (c2,c3 -cut c4) ;
consider c6 being set such that
E7: c6 in dom (c2,c3 -cut c4) and
E8: (c2,c3 -cut c4) . c6 = c5 by E6, FUNCT_1:def 5;
E9: c6 in c3 -' c2 by E7, PBOOLE:def 3;
c3 -' c2 = { b1 where B is Nat : b1 < c3 -' c2 } by AXIOMS:30;
then consider c7 being Nat such that
E10: ( c7 = c6 & c7 < c3 -' c2 ) by E9;
reconsider c8 = c6 as Nat by E10;
c5 = c4 . (c2 + c8) by E8, E9, Def1;
hence c5 in NAT ;
end;
then rng (c2,c3 -cut c4) c= NAT by TARSKI:def 3;
hence c2,c3 -cut c4 is natural-yielding by SEQM_3:def 8;
end;
end;

registration
let c1, c2, c3 be Nat;
let c4 be finite-support ManySortedSet of c1;
cluster a2,a3 -cut a4 -> finite-support ;
coherence
c2,c3 -cut c4 is finite-support ;
end;

theorem Th6: :: BAGORDER:6
for b1, b2 being Nat
for b3, b4 being ManySortedSet of b1 holds
( b3 = b4 iff ( 0,(b2 + 1) -cut b3 = 0,(b2 + 1) -cut b4 & (b2 + 1),b1 -cut b3 = (b2 + 1),b1 -cut b4 ) )
proof
let c1, c2 be Nat;
let c3, c4 be ManySortedSet of c1;
set c5 = 0,(c2 + 1) -cut c3;
set c6 = (c2 + 1),c1 -cut c3;
set c7 = 0,(c2 + 1) -cut c4;
set c8 = (c2 + 1),c1 -cut c4;
thus ( c3 = c4 implies ( 0,(c2 + 1) -cut c3 = 0,(c2 + 1) -cut c4 & (c2 + 1),c1 -cut c3 = (c2 + 1),c1 -cut c4 ) ) ;
assume E7: ( 0,(c2 + 1) -cut c3 = 0,(c2 + 1) -cut c4 & (c2 + 1),c1 -cut c3 = (c2 + 1),c1 -cut c4 ) ;
E8: now
let c9 be Nat;
assume E9: c9 in c2 + 1 ;
(c2 + 1) -' 0 = ((c2 + 1) + 0) -' 0 ;
then E10: c9 in (c2 + 1) -' 0 by E9, BINARITH:39;
then (0,(c2 + 1) -cut c4) . c9 = c4 . (0 + c9) by Def1;
hence c3 . c9 = c4 . c9 by E7, E10, Def1;
end;
E9: now
let c9 be Nat;
assume E10: ( c9 >= c2 + 1 & c9 < c1 ) ;
set c10 = c9 -' (c2 + 1);
E11: c9 - (c2 + 1) >= (c2 + 1) - (c2 + 1) by E10, XREAL_1:11;
then E12: c9 -' (c2 + 1) = c9 - (c2 + 1) by BINARITH:def 3;
c1 >= c2 + 1 by E10, XXREAL_0:2;
then c1 - (c2 + 1) >= (c2 + 1) - (c2 + 1) by XREAL_1:11;
then E13: c1 -' (c2 + 1) = c1 - (c2 + 1) by BINARITH:def 3;
c9 - (c2 + 1) < c1 - (c2 + 1) by E10, REAL_1:92;
then E14: c9 -' (c2 + 1) in c1 -' (c2 + 1) by E12, E13, EULER_1:1;
then E15: ((c2 + 1),c1 -cut c3) . (c9 -' (c2 + 1)) = c3 . ((c9 - (c2 + 1)) + (c2 + 1)) by E12, Def1;
((c2 + 1),c1 -cut c4) . (c9 -' (c2 + 1)) = c4 . ((c2 + 1) + (c9 -' (c2 + 1))) by E14, Def1;
hence c3 . c9 = c4 . c9 by E7, E11, E15, BINARITH:def 3;
end;
now
let c9 be set ;
assume E10: c9 in c1 ;
c1 = { b1 where B is Nat : b1 < c1 } by AXIOMS:30;
then consider c10 being Nat such that
E11: ( c10 = c9 & c10 < c1 ) by E10;
reconsider c11 = c9 as Nat by E11;
per cases not ( not c11 in c2 + 1 & c11 in c2 + 1 ) ;
suppose c11 in c2 + 1 ;
hence c3 . c9 = c4 . c9 by E8;
end;
suppose not c11 in c2 + 1 ;
then ( c11 >= c2 + 1 & c11 < c1 ) by E11, EULER_1:1;
hence c3 . c9 = c4 . c9 by E9;
end;
end;
end;
hence c3 = c4 by PBOOLE:3;
end;

definition
let c1 be non empty set ;
let c2 be non empty Nat;
func Fin c1,c2 -> set equals :: BAGORDER:def 2
{ b1 where B is Subset of a1 : ( b1 is finite & not b1 is empty & Card b1 <=` a2 ) } ;
coherence
{ b1 where B is Subset of c1 : ( b1 is finite & not b1 is empty & Card b1 <=` c2 ) } is set ;
end;

:: deftheorem Def2 defines Fin BAGORDER:def 2 :
for b1 being non empty set
for b2 being non empty Nat holds Fin b1,b2 = { b3 where B is Subset of b1 : ( b3 is finite & not b3 is empty & Card b3 <=` b2 ) } ;

registration
let c1 be non empty set ;
let c2 be non empty Nat;
cluster Fin a1,a2 -> non empty ;
coherence
not Fin c1,c2 is empty
proof
consider c3 being Element of c1;
E7: 0 + 1 < c2 + 1 by XREAL_1:10;
E8: now
per cases ( 1 c= c2 or c2 in 1 ) by ORDINAL1:26;
suppose 1 c= c2 ;
hence Card {c3} <=` c2 by CARD_1:79;
end;
suppose E9: c2 in 1 ;
1 = { b1 where B is Nat : b1 < 1 } by AXIOMS:30;
then consider c4 being Nat such that
E10: ( c4 = c2 & c4 < 1 ) by E9;
thus Card {c3} <=` c2 by E7, E10, NAT_1:38;
end;
end;
end;
{c3} in Fin c1,c2 by E8;
hence not Fin c1,c2 is empty ;
end;
end;

theorem Th7: :: BAGORDER:7
for b1 being non empty transitive antisymmetric RelStr
for b2 being finite Subset of b1 holds
not ( b2 <> {} & ( for b3 being Element of b1 holds
not ( b3 in b2 & b3 is_maximal_wrt b2,the InternalRel of b1 ) ) )
proof
let c1 be non empty transitive antisymmetric RelStr ;
let c2 be finite Subset of c1;
set c3 = the InternalRel of c1;
set c4 = the carrier of c1;
E8: the InternalRel of c1 is_transitive_in the carrier of c1 by ORDERS_2:def 5;
E9: the InternalRel of c1 is_antisymmetric_in the carrier of c1 by ORDERS_2:def 6;
E10: c2 is finite ;
defpred S1[ set ] means not ( a1 <> {} & ( for b1 being Element of c1 holds
not ( b1 in a1 & b1 is_maximal_wrt a1,the InternalRel of c1 ) ) );
E11: S1[ {} ] ;
now
let c5, c6 be set ;
assume that
E12: ( c5 in c2 & c6 c= c2 ) and
E13: not ( c6 <> {} & ( for b1 being Element of c1 holds
not ( b1 in c6 & b1 is_maximal_wrt c6,the InternalRel of c1 ) ) ) ;
reconsider c7 = c5 as Element of c1 by E12;
assume c6 \/ {c5} <> {} ;
per cases not ( not c6 = {} & not c6 <> {} ) ;
suppose E14: c6 = {} ;
take c8 = c7;
thus c8 in c6 \/ {c5} by E14, TARSKI:def 1;
( c8 in c6 \/ {c5} & ( for b1 being set holds
not ( b1 in c6 \/ {c8} & b1 <> c8 & [c8,b1] in the InternalRel of c1 ) ) ) by E14, TARSKI:def 1;
hence c8 is_maximal_wrt c6 \/ {c5},the InternalRel of c1 by WAYBEL_4:def 24;
end;
suppose c6 <> {} ;
then consider c8 being Element of c1 such that
E14: ( c8 in c6 & c8 is_maximal_wrt c6,the InternalRel of c1 ) by E13;
now
per cases not ( not [c8,c5] in the InternalRel of c1 & not [c5,c8] in the InternalRel of c1 & not ( not [c8,c5] in the InternalRel of c1 & not [c5,c8] in the InternalRel of c1 ) ) ;
suppose E15: [c8,c5] in the InternalRel of c1 ;
take c9 = c7;
E16: c5 in {c5} by TARSKI:def 1;
hence c9 in c6 \/ {c5} by XBOOLE_0:def 2;
now
thus c9 in c6 \/ {c5} by E16, XBOOLE_0:def 2;
now
assume ex b1 being set st
( b1 in c6 \/ {c5} & b1 <> c5 & [c5,b1] in the InternalRel of c1 ) ;
then consider c10 being set such that
E17: ( c10 in c6 \/ {c5} & c10 <> c5 & [c5,c10] in the InternalRel of c1 ) ;
( c8 in the carrier of c1 & c9 in the carrier of c1 & c10 in the carrier of c1 ) by E17, ZFMISC_1:106;
then E18: [c8,c10] in the InternalRel of c1 by E8, E15, E17, RELAT_2:def 8;
per cases ( c10 in c6 or c10 in {c5} ) by E17, XBOOLE_0:def 2;
suppose E19: c10 in c6 ;
now
per cases not ( not c10 = c8 & not c10 <> c8 ) ;
suppose E20: c10 = c8 ;
then c8 = c9 by E9, E15, E17, RELAT_2:def 4;
hence not verum by E17, E20;
end;
suppose c10 <> c8 ;
hence not verum by E14, E18, E19, WAYBEL_4:def 24;
end;
end;
end;
hence not verum ;
end;
suppose c10 in {c5} ;
hence not verum by E17, TARSKI:def 1;
end;
end;
end;
hence for b1 being set holds
not ( b1 in c6 \/ {c5} & b1 <> c5 & [c5,b1] in the InternalRel of c1 ) ;
end;
hence c9 is_maximal_wrt c6 \/ {c5},the InternalRel of c1 by WAYBEL_4:def 24;
end;
suppose E15: [c5,c8] in the InternalRel of c1 ;
take c9 = c8;
thus c9 in c6 \/ {c5} by E14, XBOOLE_0:def 2;
now
thus c9 in c6 \/ {c5} by E14, XBOOLE_0:def 2;
now
assume ex b1 being set st
( b1 in c6 \/ {c5} & b1 <> c9 & [c9,b1] in the InternalRel of c1 ) ;
then consider c10 being set such that
E16: ( c10 in c6 \/ {c5} & c10 <> c9 & [c9,c10] in the InternalRel of c1 ) ;
per cases ( c10 in c6 or c10 in {c5} ) by E16, XBOOLE_0:def 2;
suppose c10 in c6 ;
hence not verum by E14, E16, WAYBEL_4:def 24;
end;
suppose c10 in {c5} ;
then E17: c10 = c5 by TARSKI:def 1;
c10 in the carrier of c1 by E16, ZFMISC_1:106;
hence not verum by E9, E15, E16, E17, RELAT_2:def 4;
end;
end;
end;
hence for b1 being set holds
not ( b1 in c6 \/ {c5} & b1 <> c9 & [c9,b1] in the InternalRel of c1 ) ;
end;
hence c9 is_maximal_wrt c6 \/ {c5},the InternalRel of c1 by WAYBEL_4:def 24;
end;
suppose E15: ( not [c8,c5] in the InternalRel of c1 & not [c5,c8] in the InternalRel of c1 ) ;
take c9 = c8;
thus c9 in c6 \/ {c5} by E14, XBOOLE_0:def 2;
now
thus c9 in c6 \/ {c5} by E14, XBOOLE_0:def 2;
now
assume ex b1 being set st
( b1 in c6 \/ {c5} & b1 <> c9 & [c9,b1] in the InternalRel of c1 ) ;
then consider c10 being set such that
E16: ( c10 in c6 \/ {c5} & c10 <> c9 & [c9,c10] in the InternalRel of c1 ) ;
per cases ( c10 in c6 or c10 in {c5} ) by E16, XBOOLE_0:def 2;
suppose c10 in c6 ;
hence not verum by E14, E16, WAYBEL_4:def 24;
end;
suppose c10 in {c5} ;
hence not verum by E15, E16, TARSKI:def 1;
end;
end;
end;
hence for b1 being set holds
not ( b1 in c6 \/ {c5} & b1 <> c9 & [c9,b1] in the InternalRel of c1 ) ;
end;
hence c9 is_maximal_wrt c6 \/ {c5},the InternalRel of c1 by WAYBEL_4:def 24;
end;
end;
end;
hence ex b1 being Element of c1 st
( b1 in c6 \/ {c5} & b1 is_maximal_wrt c6 \/ {c5},the InternalRel of c1 ) ;
end;
end;
end;
then E12: for b1, b2 being set holds
( b1 in c2 & b2 c= c2 & S1[b2] implies S1[b2 \/ {b1}] ) ;
thus S1[c2] from FINSET_1:sch 2(E10, E11, E12);
end;

theorem Th8: :: BAGORDER:8
for b1 being non empty transitive antisymmetric RelStr
for b2 being finite Subset of b1 holds
not ( b2 <> {} & ( for b3 being Element of b1 holds
not ( b3 in b2 & b3 is_minimal_wrt b2,the InternalRel of b1 ) ) )
proof
let c1 be non empty transitive antisymmetric RelStr ;
let c2 be finite Subset of c1;
set c3 = the InternalRel of c1;
set c4 = the carrier of c1;
E9: the InternalRel of c1 is_transitive_in the carrier of c1 by ORDERS_2:def 5;
E10: the InternalRel of c1 is_antisymmetric_in the carrier of c1 by ORDERS_2:def 6;
E11: c2 is finite ;
defpred S1[ set ] means not ( a1 <> {} & ( for b1 being Element of c1 holds
not ( b1 in a1 & b1 is_minimal_wrt a1,the InternalRel of c1 ) ) );
E12: S1[ {} ] ;
now
let c5, c6 be set ;
assume that
E13: ( c5 in c2 & c6 c= c2 ) and
E14: not ( c6 <> {} & ( for b1 being Element of c1 holds
not ( b1 in c6 & b1 is_minimal_wrt c6,the InternalRel of c1 ) ) ) ;
reconsider c7 = c5 as Element of c1 by E13;
assume c6 \/ {c5} <> {} ;
per cases not ( not c6 = {} & not c6 <> {} ) ;
suppose E15: c6 = {} ;
take c8 = c7;
thus c8 in c6 \/ {c5} by E15, TARSKI:def 1;
( c8 in c6 \/ {c5} & ( for b1 being set holds
not ( b1 in c6 \/ {c8} & b1 <> c8 & [b1,c8] in the InternalRel of c1 ) ) ) by E15, TARSKI:def 1;
hence c8 is_minimal_wrt c6 \/ {c5},the InternalRel of c1 by WAYBEL_4:def 26;
end;
suppose c6 <> {} ;
then consider c8 being Element of c1 such that
E15: ( c8 in c6 & c8 is_minimal_wrt c6,the InternalRel of c1 ) by E14;
now
per cases not ( not [c5,c8] in the InternalRel of c1 & not [c8,c5] in the InternalRel of c1 & not ( not [c8,c5] in the InternalRel of c1 & not [c5,c8] in the InternalRel of c1 ) ) ;
suppose E16: [c5,c8] in the InternalRel of c1 ;
take c9 = c7;
E17: c5 in {c5} by TARSKI:def 1;
hence c9 in c6 \/ {c5} by XBOOLE_0:def 2;
now
thus c9 in c6 \/ {c5} by E17, XBOOLE_0:def 2;
now
assume ex b1 being set st
( b1 in c6 \/ {c5} & b1 <> c5 & [b1,c5] in the InternalRel of c1 ) ;
then consider c10 being set such that
E18: ( c10 in c6 \/ {c5} & c10 <> c5 & [c10,c5] in the InternalRel of c1 ) ;
( c8 in the carrier of c1 & c9 in the carrier of c1 & c10 in the carrier of c1 ) by E18, ZFMISC_1:106;
then E19: [c10,c8] in the InternalRel of c1 by E9, E16, E18, RELAT_2:def 8;
per cases ( c10 in c6 or c10 in {c5} ) by E18, XBOOLE_0:def 2;
suppose E20: c10 in c6 ;
now
per cases not ( not c10 = c8 & not c10 <> c8 ) ;
suppose E21: c10 = c8 ;
then c8 = c9 by E10, E16, E18, RELAT_2:def 4;
hence not verum by E18, E21;
end;
suppose c10 <> c8 ;
hence not verum by E15, E19, E20, WAYBEL_4:def 26;
end;
end;
end;
hence not verum ;
end;
suppose c10 in {c5} ;
hence not verum by E18, TARSKI:def 1;
end;
end;
end;
hence for b1 being set holds
not ( b1 in c6 \/ {c5} & b1 <> c5 & [b1,c5] in the InternalRel of c1 ) ;
end;
hence c9 is_minimal_wrt c6 \/ {c5},the InternalRel of c1 by WAYBEL_4:def 26;
end;
suppose E16: [c8,c5] in the InternalRel of c1 ;
take c9 = c8;
thus c9 in c6 \/ {c5} by E15, XBOOLE_0:def 2;
now
thus c9 in c6 \/ {c5} by E15, XBOOLE_0:def 2;
now
assume ex b1 being set st
( b1 in c6 \/ {c5} & b1 <> c9 & [b1,c9] in the InternalRel of c1 ) ;
then consider c10 being set such that
E17: ( c10 in c6 \/ {c5} & c10 <> c9 & [c10,c9] in the InternalRel of c1 ) ;
per cases ( c10 in c6 or c10 in {c5} ) by E17, XBOOLE_0:def 2;
suppose c10 in c6 ;
hence not verum by E15, E17, WAYBEL_4:def 26;
end;
suppose c10 in {c5} ;
then E18: c10 = c5 by TARSKI:def 1;
c10 in the carrier of c1 by E17, ZFMISC_1:106;
hence not verum by E10, E16, E17, E18, RELAT_2:def 4;
end;
end;
end;
hence for b1 being set holds
not ( b1 in c6 \/ {c5} & b1 <> c9 & [b1,c9] in the InternalRel of c1 ) ;
end;
hence c9 is_minimal_wrt c6 \/ {c5},the InternalRel of c1 by WAYBEL_4:def 26;
end;