let X be set ; :: thesis: for Y, Z being finite Subset-Family of X st Z is in_general_position & Y c= Z holds

Y is in_general_position

let Y, Z be finite Subset-Family of X; :: thesis: ( Z is in_general_position & Y c= Z implies Y is in_general_position )

assume that

A1: Z is in_general_position and

A2: Y c= Z ; :: thesis: Y is in_general_position

A3: not {} in Components Z by A1;

not {} in Components Y

Y is in_general_position

let Y, Z be finite Subset-Family of X; :: thesis: ( Z is in_general_position & Y c= Z implies Y is in_general_position )

assume that

A1: Z is in_general_position and

A2: Y c= Z ; :: thesis: Y is in_general_position

A3: not {} in Components Z by A1;

not {} in Components Y

proof

hence
Y is in_general_position
; :: thesis: verum
deffunc H_{1}( set ) -> Element of BOOLEAN = TRUE ;

consider p being FinSequence of bool X such that

A4: len p = card Y and

A5: rng p = Y and

A6: Components Y = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } by Def2;

A7: p is one-to-one by A4, A5, FINSEQ_4:62;

then A8: rng p = dom (p ") by FUNCT_1:33;

consider p1 being FinSequence of bool X such that

A9: len p1 = card Z and

A10: rng p1 = Z and

A11: Components Z = { (Intersect (rng (MergeSequence (p1,q)))) where q is FinSequence of BOOLEAN : len q = len p1 } by Def2;

defpred S_{1}[ set ] means p1 . $1 in rng p;

assume {} in Components Y ; :: thesis: contradiction

then consider q being FinSequence of BOOLEAN such that

A12: {} = Intersect (rng (MergeSequence (p,q))) and

A13: len q = len p by A6;

deffunc H_{2}( set ) -> set = ((q * (p ")) * p1) . $1;

A14: dom p = rng (p ") by A7, FUNCT_1:33;

A15: for i being Nat st i in Seg (len p1) holds

( ( S_{1}[i] implies H_{2}(i) in BOOLEAN ) & ( not S_{1}[i] implies H_{1}(i) in BOOLEAN ) )

A19: len q1 = len p1 and

A20: for i being Nat st i in Seg (len p1) holds

( ( S_{1}[i] implies q1 . i = H_{2}(i) ) & ( not S_{1}[i] implies q1 . i = H_{1}(i) ) )
from YELLOW15:sch 1(A15);

A21: p1 is one-to-one by A9, A10, FINSEQ_4:62;

then A22: rng p1 = dom (p1 ") by FUNCT_1:33;

rng (MergeSequence (p,q)) c= rng (MergeSequence (p1,q1))

hence contradiction by A3, A11, A19; :: thesis: verum

end;consider p being FinSequence of bool X such that

A4: len p = card Y and

A5: rng p = Y and

A6: Components Y = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } by Def2;

A7: p is one-to-one by A4, A5, FINSEQ_4:62;

then A8: rng p = dom (p ") by FUNCT_1:33;

consider p1 being FinSequence of bool X such that

A9: len p1 = card Z and

A10: rng p1 = Z and

A11: Components Z = { (Intersect (rng (MergeSequence (p1,q)))) where q is FinSequence of BOOLEAN : len q = len p1 } by Def2;

defpred S

assume {} in Components Y ; :: thesis: contradiction

then consider q being FinSequence of BOOLEAN such that

A12: {} = Intersect (rng (MergeSequence (p,q))) and

A13: len q = len p by A6;

deffunc H

A14: dom p = rng (p ") by A7, FUNCT_1:33;

A15: for i being Nat st i in Seg (len p1) holds

( ( S

proof

consider q1 being FinSequence of BOOLEAN such that
let i be Nat; :: thesis: ( i in Seg (len p1) implies ( ( S_{1}[i] implies H_{2}(i) in BOOLEAN ) & ( not S_{1}[i] implies H_{1}(i) in BOOLEAN ) ) )

assume i in Seg (len p1) ; :: thesis: ( ( S_{1}[i] implies H_{2}(i) in BOOLEAN ) & ( not S_{1}[i] implies H_{1}(i) in BOOLEAN ) )

then A16: i in dom p1 by FINSEQ_1:def 3;

thus ( p1 . i in rng p implies ((q * (p ")) * p1) . i in BOOLEAN ) :: thesis: ( not S_{1}[i] implies H_{1}(i) in BOOLEAN )_{1}[i] implies H_{1}(i) in BOOLEAN )
; :: thesis: verum

end;assume i in Seg (len p1) ; :: thesis: ( ( S

then A16: i in dom p1 by FINSEQ_1:def 3;

thus ( p1 . i in rng p implies ((q * (p ")) * p1) . i in BOOLEAN ) :: thesis: ( not S

proof

thus
( not S
assume A17:
p1 . i in rng p
; :: thesis: ((q * (p ")) * p1) . i in BOOLEAN

rng (p ") = dom q by A13, A14, FINSEQ_3:29;

then p1 . i in dom (q * (p ")) by A8, A17, RELAT_1:27;

then A18: (q * (p ")) . (p1 . i) in rng (q * (p ")) by FUNCT_1:def 3;

dom (q * (p ")) c= rng p by A8, RELAT_1:25;

then rng (q * (p ")) = rng ((q * (p ")) * p1) by A2, A5, A10, RELAT_1:28, XBOOLE_1:1;

then ((q * (p ")) * p1) . i in rng ((q * (p ")) * p1) by A16, A18, FUNCT_1:13;

hence ((q * (p ")) * p1) . i in BOOLEAN ; :: thesis: verum

end;rng (p ") = dom q by A13, A14, FINSEQ_3:29;

then p1 . i in dom (q * (p ")) by A8, A17, RELAT_1:27;

then A18: (q * (p ")) . (p1 . i) in rng (q * (p ")) by FUNCT_1:def 3;

dom (q * (p ")) c= rng p by A8, RELAT_1:25;

then rng (q * (p ")) = rng ((q * (p ")) * p1) by A2, A5, A10, RELAT_1:28, XBOOLE_1:1;

then ((q * (p ")) * p1) . i in rng ((q * (p ")) * p1) by A16, A18, FUNCT_1:13;

hence ((q * (p ")) * p1) . i in BOOLEAN ; :: thesis: verum

A19: len q1 = len p1 and

A20: for i being Nat st i in Seg (len p1) holds

( ( S

A21: p1 is one-to-one by A9, A10, FINSEQ_4:62;

then A22: rng p1 = dom (p1 ") by FUNCT_1:33;

rng (MergeSequence (p,q)) c= rng (MergeSequence (p1,q1))

proof

then
{} = Intersect (rng (MergeSequence (p1,q1)))
by A12, SETFAM_1:44, XBOOLE_1:3;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (MergeSequence (p,q)) or z in rng (MergeSequence (p1,q1)) )

assume z in rng (MergeSequence (p,q)) ; :: thesis: z in rng (MergeSequence (p1,q1))

then consider i being Nat such that

A23: i in dom (MergeSequence (p,q)) and

A24: (MergeSequence (p,q)) . i = z by FINSEQ_2:10;

i in Seg (len (MergeSequence (p,q))) by A23, FINSEQ_1:def 3;

then i in Seg (len p) by Def1;

then A25: i in dom p by FINSEQ_1:def 3;

then A26: i in dom ((p1 ") * p) by A2, A5, A10, A22, RELAT_1:27;

then ((p1 ") * p) . i in rng ((p1 ") * p) by FUNCT_1:def 3;

then A27: ((p1 ") * p) . i in rng (p1 ") by FUNCT_1:14;

then A28: ((p1 ") * p) . i in dom p1 by A21, FUNCT_1:33;

then reconsider j = ((p1 ") * p) . i as Element of NAT ;

p1 . j = (p1 * ((p1 ") * p)) . i by A26, FUNCT_1:13

.= ((p1 * (p1 ")) * p) . i by RELAT_1:36

.= ((id (rng p1)) * p) . i by A21, FUNCT_1:39

.= p . i by A2, A5, A10, RELAT_1:53 ;

then A29: p1 . j in rng p by A25, FUNCT_1:def 3;

j in Seg (len p1) by A28, FINSEQ_1:def 3;

then A30: q1 . j = ((q * (p ")) * p1) . (((p1 ") * p) . i) by A20, A29

.= (((q * (p ")) * p1) * ((p1 ") * p)) . i by A26, FUNCT_1:13

.= ((q * (p ")) * (p1 * ((p1 ") * p))) . i by RELAT_1:36

.= ((q * (p ")) * ((p1 * (p1 ")) * p)) . i by RELAT_1:36

.= ((q * (p ")) * ((id (rng p1)) * p)) . i by A21, FUNCT_1:39

.= ((q * (p ")) * p) . i by A2, A5, A10, RELAT_1:53

.= (q * ((p ") * p)) . i by RELAT_1:36

.= (q * (id (dom p))) . i by A7, FUNCT_1:39

.= (q * (id (dom q))) . i by A13, FINSEQ_3:29

.= q . i by RELAT_1:52 ;

A31: j in dom p1 by A21, A27, FUNCT_1:33;

hence z in rng (MergeSequence (p1,q1)) by A32, FUNCT_1:def 3; :: thesis: verum

end;assume z in rng (MergeSequence (p,q)) ; :: thesis: z in rng (MergeSequence (p1,q1))

then consider i being Nat such that

A23: i in dom (MergeSequence (p,q)) and

A24: (MergeSequence (p,q)) . i = z by FINSEQ_2:10;

i in Seg (len (MergeSequence (p,q))) by A23, FINSEQ_1:def 3;

then i in Seg (len p) by Def1;

then A25: i in dom p by FINSEQ_1:def 3;

then A26: i in dom ((p1 ") * p) by A2, A5, A10, A22, RELAT_1:27;

then ((p1 ") * p) . i in rng ((p1 ") * p) by FUNCT_1:def 3;

then A27: ((p1 ") * p) . i in rng (p1 ") by FUNCT_1:14;

then A28: ((p1 ") * p) . i in dom p1 by A21, FUNCT_1:33;

then reconsider j = ((p1 ") * p) . i as Element of NAT ;

p1 . j = (p1 * ((p1 ") * p)) . i by A26, FUNCT_1:13

.= ((p1 * (p1 ")) * p) . i by RELAT_1:36

.= ((id (rng p1)) * p) . i by A21, FUNCT_1:39

.= p . i by A2, A5, A10, RELAT_1:53 ;

then A29: p1 . j in rng p by A25, FUNCT_1:def 3;

j in Seg (len p1) by A28, FINSEQ_1:def 3;

then A30: q1 . j = ((q * (p ")) * p1) . (((p1 ") * p) . i) by A20, A29

.= (((q * (p ")) * p1) * ((p1 ") * p)) . i by A26, FUNCT_1:13

.= ((q * (p ")) * (p1 * ((p1 ") * p))) . i by RELAT_1:36

.= ((q * (p ")) * ((p1 * (p1 ")) * p)) . i by RELAT_1:36

.= ((q * (p ")) * ((id (rng p1)) * p)) . i by A21, FUNCT_1:39

.= ((q * (p ")) * p) . i by A2, A5, A10, RELAT_1:53

.= (q * ((p ") * p)) . i by RELAT_1:36

.= (q * (id (dom p))) . i by A7, FUNCT_1:39

.= (q * (id (dom q))) . i by A13, FINSEQ_3:29

.= q . i by RELAT_1:52 ;

A31: j in dom p1 by A21, A27, FUNCT_1:33;

A32: now :: thesis: z = (MergeSequence (p1,q1)) . jend;

j in dom (MergeSequence (p1,q1))
by A28, Th1;per cases
( q . i = TRUE or q . i = FALSE )
by XBOOLEAN:def 3;

end;

suppose A33:
q . i = TRUE
; :: thesis: z = (MergeSequence (p1,q1)) . j

hence z =
p . i
by A24, Th2

.= ((id (rng p1)) * p) . i by A2, A5, A10, RELAT_1:53

.= ((p1 * (p1 ")) * p) . i by A21, FUNCT_1:39

.= (p1 * ((p1 ") * p)) . i by RELAT_1:36

.= p1 . j by A26, FUNCT_1:13

.= (MergeSequence (p1,q1)) . j by A30, A33, Th2 ;

:: thesis: verum

end;.= ((id (rng p1)) * p) . i by A2, A5, A10, RELAT_1:53

.= ((p1 * (p1 ")) * p) . i by A21, FUNCT_1:39

.= (p1 * ((p1 ") * p)) . i by RELAT_1:36

.= p1 . j by A26, FUNCT_1:13

.= (MergeSequence (p1,q1)) . j by A30, A33, Th2 ;

:: thesis: verum

suppose A34:
q . i = FALSE
; :: thesis: z = (MergeSequence (p1,q1)) . j

hence z =
X \ (p . i)
by A24, A25, Th3

.= X \ (((id (rng p1)) * p) . i) by A2, A5, A10, RELAT_1:53

.= X \ (((p1 * (p1 ")) * p) . i) by A21, FUNCT_1:39

.= X \ ((p1 * ((p1 ") * p)) . i) by RELAT_1:36

.= X \ (p1 . j) by A26, FUNCT_1:13

.= (MergeSequence (p1,q1)) . j by A31, A30, A34, Th3 ;

:: thesis: verum

end;.= X \ (((id (rng p1)) * p) . i) by A2, A5, A10, RELAT_1:53

.= X \ (((p1 * (p1 ")) * p) . i) by A21, FUNCT_1:39

.= X \ ((p1 * ((p1 ") * p)) . i) by RELAT_1:36

.= X \ (p1 . j) by A26, FUNCT_1:13

.= (MergeSequence (p1,q1)) . j by A31, A30, A34, Th3 ;

:: thesis: verum

hence z in rng (MergeSequence (p1,q1)) by A32, FUNCT_1:def 3; :: thesis: verum

hence contradiction by A3, A11, A19; :: thesis: verum