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

proof

deffunc H₁( 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₁[ 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₂( 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₁[i] implies H₂(i) in BOOLEAN ) & ( not S₁[i] implies H₁(i) in BOOLEAN ) )

proof

let i be Nat; :: thesis: ( i in Seg (len p1) implies ( ( S₁[i] implies H₂(i) in BOOLEAN ) & ( not S₁[i] implies H₁(i) in BOOLEAN ) ) )
assume i in Seg (len p1) ; :: thesis: ( ( S₁[i] implies H₂(i) in BOOLEAN ) & ( not S₁[i] implies H₁(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₁[i] implies H₁(i) in BOOLEAN )

proof

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;

thus ( not S₁[i] implies H₁(i) in BOOLEAN ) ; :: thesis: verum

end;

consider q1 being FinSequence of BOOLEAN such that
A19: len q1 = len p1 and
A20: for i being Nat st i in Seg (len p1) holds
( ( S₁[i] implies q1 . i = H₂(i) ) & ( not S₁[i] implies q1 . i = H₁(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))

proof

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;

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

per cases ( q . i = TRUE or q . i = FALSE ) by XBOOLEAN:def 3;

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;

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;

end;

end;

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

end;

then {} = Intersect (rng (MergeSequence (p1,q1))) by A12, SETFAM_1:44, XBOOLE_1:3;
hence contradiction by A3, A11, A19; :: thesis: verum

end;

hence Y is in_general_position ; :: thesis: verum