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:
A3: not {} in Components Z by A1;
not {} in Components Y
proof
deffunc H1( 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 ;
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 S1[ 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 H2( set ) -> set = ((q * (p ")) * p1) . \$1;
A14: dom p = rng (p ") by ;
A15: for i being Nat st i in Seg (len p1) holds
( ( S1[i] implies H2(i) in BOOLEAN ) & ( not S1[i] implies H1(i) in BOOLEAN ) )
proof
let i be Nat; :: thesis: ( i in Seg (len p1) implies ( ( S1[i] implies H2(i) in BOOLEAN ) & ( not S1[i] implies H1(i) in BOOLEAN ) ) )
assume i in Seg (len p1) ; :: thesis: ( ( S1[i] implies H2(i) in BOOLEAN ) & ( not S1[i] implies H1(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 S1[i] implies H1(i) in BOOLEAN )
proof
assume A17: p1 . i in rng p ; :: thesis: ((q * (p ")) * p1) . i in BOOLEAN
rng (p ") = dom q by ;
then p1 . i in dom (q * (p ")) by ;
then A18: (q * (p ")) . (p1 . i) in rng (q * (p ")) by FUNCT_1:def 3;
dom (q * (p ")) c= rng p by ;
then rng (q * (p ")) = rng ((q * (p ")) * p1) by ;
then ((q * (p ")) * p1) . i in rng ((q * (p ")) * p1) by ;
hence ((q * (p ")) * p1) . i in BOOLEAN ; :: thesis: verum
end;
thus ( not S1[i] implies H1(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
( ( S1[i] implies q1 . i = H2(i) ) & ( not S1[i] implies q1 . i = H1(i) ) ) from A21: p1 is one-to-one by ;
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 ;
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 ;
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 ;
then reconsider j = ((p1 ") * p) . i as Element of NAT ;
p1 . j = (p1 * ((p1 ") * p)) . i by
.= ((p1 * (p1 ")) * p) . i by RELAT_1:36
.= ((id (rng p1)) * p) . i by
.= p . i by ;
then A29: p1 . j in rng p by ;
j in Seg (len p1) by ;
then A30: q1 . j = ((q * (p ")) * p1) . (((p1 ") * p) . i) by
.= (((q * (p ")) * p1) * ((p1 ") * p)) . i by
.= ((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
.= ((q * (p ")) * p) . i by
.= (q * ((p ") * p)) . i by RELAT_1:36
.= (q * (id (dom p))) . i by
.= (q * (id (dom q))) . i by
.= q . i by RELAT_1:52 ;
A31: j in dom p1 by ;
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
.= ((id (rng p1)) * p) . i by
.= ((p1 * (p1 ")) * p) . i by
.= (p1 * ((p1 ") * p)) . i by RELAT_1:36
.= p1 . j by
.= (MergeSequence (p1,q1)) . j by ;
:: thesis: verum
end;
suppose A34: q . i = FALSE ; :: thesis: z = (MergeSequence (p1,q1)) . j
hence z = X \ (p . i) by
.= X \ (((id (rng p1)) * p) . i) by
.= X \ (((p1 * (p1 ")) * p) . i) by
.= X \ ((p1 * ((p1 ") * p)) . i) by RELAT_1:36
.= X \ (p1 . j) by
.= (MergeSequence (p1,q1)) . j by A31, A30, A34, Th3 ;
:: thesis: verum
end;
end;
end;
j in dom (MergeSequence (p1,q1)) by ;
hence z in rng (MergeSequence (p1,q1)) by ; :: thesis: verum
end;
then {} = Intersect (rng (MergeSequence (p1,q1))) by ;
hence contradiction by A3, A11, A19; :: thesis: verum
end;
hence Y is in_general_position ; :: thesis: verum