let k be Element of NAT ; :: thesis: for X being non empty set st 0 < k & k + 1 c= card X holds

for A1, A2, A3, A4, A5, A6 being POINT of (G_ (k,X))

for L1, L2, L3, L4 being LINE of (G_ (k,X)) st A1 on L1 & A2 on L1 & A3 on L2 & A4 on L2 & A5 on L1 & A5 on L2 & A1 on L3 & A3 on L3 & A2 on L4 & A4 on L4 & not A5 on L3 & not A5 on L4 & L1 <> L2 & L3 <> L4 holds

ex A6 being POINT of (G_ (k,X)) st

( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) )

let X be non empty set ; :: thesis: ( 0 < k & k + 1 c= card X implies for A1, A2, A3, A4, A5, A6 being POINT of (G_ (k,X))

for L1, L2, L3, L4 being LINE of (G_ (k,X)) st A1 on L1 & A2 on L1 & A3 on L2 & A4 on L2 & A5 on L1 & A5 on L2 & A1 on L3 & A3 on L3 & A2 on L4 & A4 on L4 & not A5 on L3 & not A5 on L4 & L1 <> L2 & L3 <> L4 holds

ex A6 being POINT of (G_ (k,X)) st

( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) ) )

assume that

A1: 0 < k and

A2: k + 1 c= card X ; :: thesis: for A1, A2, A3, A4, A5, A6 being POINT of (G_ (k,X))

for L1, L2, L3, L4 being LINE of (G_ (k,X)) st A1 on L1 & A2 on L1 & A3 on L2 & A4 on L2 & A5 on L1 & A5 on L2 & A1 on L3 & A3 on L3 & A2 on L4 & A4 on L4 & not A5 on L3 & not A5 on L4 & L1 <> L2 & L3 <> L4 holds

ex A6 being POINT of (G_ (k,X)) st

( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) )

A3: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by A1, A2, Def1;

A4: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by A1, A2, Def1;

let A1, A2, A3, A4, A5, A6 be POINT of (G_ (k,X)); :: thesis: for L1, L2, L3, L4 being LINE of (G_ (k,X)) st A1 on L1 & A2 on L1 & A3 on L2 & A4 on L2 & A5 on L1 & A5 on L2 & A1 on L3 & A3 on L3 & A2 on L4 & A4 on L4 & not A5 on L3 & not A5 on L4 & L1 <> L2 & L3 <> L4 holds

ex A6 being POINT of (G_ (k,X)) st

( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) )

let L1, L2, L3, L4 be LINE of (G_ (k,X)); :: thesis: ( A1 on L1 & A2 on L1 & A3 on L2 & A4 on L2 & A5 on L1 & A5 on L2 & A1 on L3 & A3 on L3 & A2 on L4 & A4 on L4 & not A5 on L3 & not A5 on L4 & L1 <> L2 & L3 <> L4 implies ex A6 being POINT of (G_ (k,X)) st

( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) ) )

assume that

A5: A1 on L1 and

A6: A2 on L1 and

A7: A3 on L2 and

A8: A4 on L2 and

A9: A5 on L1 and

A10: A5 on L2 and

A11: A1 on L3 and

A12: A3 on L3 and

A13: A2 on L4 and

A14: A4 on L4 and

A15: not A5 on L3 and

A16: not A5 on L4 and

A17: L1 <> L2 and

A18: L3 <> L4 ; :: thesis: ex A6 being POINT of (G_ (k,X)) st

( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) )

A19: ( A1 c= L1 & A2 c= L1 ) by A1, A2, A5, A6, Th10;

A20: ( A3 c= L2 & A4 c= L2 ) by A1, A2, A7, A8, Th10;

A21: ( A5 c= L1 & A5 c= L2 ) by A1, A2, A9, A10, Th10;

A5 in the Points of (G_ (k,X)) ;

then A22: ex B5 being Subset of X st

( B5 = A5 & card B5 = k ) by A3;

A2 in the Points of (G_ (k,X)) ;

then A23: ex B2 being Subset of X st

( B2 = A2 & card B2 = k ) by A3;

then A24: A2 is finite ;

reconsider k1 = k - 1 as Element of NAT by A1, NAT_1:20;

L3 in the Lines of (G_ (k,X)) ;

then A25: ex K3 being Subset of X st

( K3 = L3 & card K3 = k + 1 ) by A4;

then A26: L3 is finite ;

L4 in the Lines of (G_ (k,X)) ;

then ex K4 being Subset of X st

( K4 = L4 & card K4 = k + 1 ) by A4;

then card (L3 /\ L4) in Segm (k + 1) by A25, A18, Th1;

then card (L3 /\ L4) in succ (Segm k) by NAT_1:38;

then A27: card (L3 /\ L4) c= k by ORDINAL1:22;

A1 in the Points of (G_ (k,X)) ;

then A28: ex B1 being Subset of X st

( B1 = A1 & card B1 = k ) by A3;

then A29: A1 is finite ;

G_ (k,X) is Vebleian by A1, A2, Th11;

then consider A6 being POINT of (G_ (k,X)) such that

A30: A6 on L3 and

A31: A6 on L4 by A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17;

A6 in the Points of (G_ (k,X)) ;

then A32: ex a6 being Subset of X st

( a6 = A6 & card a6 = k ) by A3;

then A33: A6 is finite ;

A34: ( A6 c= L3 & A6 c= L4 ) by A1, A2, A30, A31, Th10;

then A6 c= L3 /\ L4 by XBOOLE_1:19;

then k c= card (L3 /\ L4) by A32, CARD_1:11;

then card (L3 /\ L4) = k by A27, XBOOLE_0:def 10;

then A35: L3 /\ L4 = A6 by A32, A34, A26, CARD_2:102, XBOOLE_1:19;

L2 in the Lines of (G_ (k,X)) ;

then A36: ex K2 being Subset of X st

( K2 = L2 & card K2 = k + 1 ) by A4;

then A37: L2 is finite ;

A4 in the Points of (G_ (k,X)) ;

then A38: ex B4 being Subset of X st

( B4 = A4 & card B4 = k ) by A3;

then A39: A4 is finite ;

L1 in the Lines of (G_ (k,X)) ;

then A40: ex K1 being Subset of X st

( K1 = L1 & card K1 = k + 1 ) by A4;

then A41: L1 is finite ;

A3 in the Points of (G_ (k,X)) ;

then A42: ex B3 being Subset of X st

( B3 = A3 & card B3 = k ) by A3;

then A43: A3 is finite ;

A44: ( A3 c= L3 & A4 c= L4 ) by A1, A2, A12, A14, Th10;

then A45: A3 /\ A4 c= A6 by A35, XBOOLE_1:27;

A46: ( A1 c= L3 & A2 c= L4 ) by A1, A2, A11, A13, Th10;

then A47: A1 /\ A2 c= A6 by A35, XBOOLE_1:27;

then A48: (A1 /\ A2) \/ (A3 /\ A4) c= A6 by A45, XBOOLE_1:8;

A49: ( not A6 on L1 implies A6 = (A1 /\ A2) \/ (A3 /\ A4) )

( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) ) by A30, A31, A49; :: thesis: verum

for A1, A2, A3, A4, A5, A6 being POINT of (G_ (k,X))

for L1, L2, L3, L4 being LINE of (G_ (k,X)) st A1 on L1 & A2 on L1 & A3 on L2 & A4 on L2 & A5 on L1 & A5 on L2 & A1 on L3 & A3 on L3 & A2 on L4 & A4 on L4 & not A5 on L3 & not A5 on L4 & L1 <> L2 & L3 <> L4 holds

ex A6 being POINT of (G_ (k,X)) st

( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) )

let X be non empty set ; :: thesis: ( 0 < k & k + 1 c= card X implies for A1, A2, A3, A4, A5, A6 being POINT of (G_ (k,X))

for L1, L2, L3, L4 being LINE of (G_ (k,X)) st A1 on L1 & A2 on L1 & A3 on L2 & A4 on L2 & A5 on L1 & A5 on L2 & A1 on L3 & A3 on L3 & A2 on L4 & A4 on L4 & not A5 on L3 & not A5 on L4 & L1 <> L2 & L3 <> L4 holds

ex A6 being POINT of (G_ (k,X)) st

( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) ) )

assume that

A1: 0 < k and

A2: k + 1 c= card X ; :: thesis: for A1, A2, A3, A4, A5, A6 being POINT of (G_ (k,X))

for L1, L2, L3, L4 being LINE of (G_ (k,X)) st A1 on L1 & A2 on L1 & A3 on L2 & A4 on L2 & A5 on L1 & A5 on L2 & A1 on L3 & A3 on L3 & A2 on L4 & A4 on L4 & not A5 on L3 & not A5 on L4 & L1 <> L2 & L3 <> L4 holds

ex A6 being POINT of (G_ (k,X)) st

( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) )

A3: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by A1, A2, Def1;

A4: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by A1, A2, Def1;

let A1, A2, A3, A4, A5, A6 be POINT of (G_ (k,X)); :: thesis: for L1, L2, L3, L4 being LINE of (G_ (k,X)) st A1 on L1 & A2 on L1 & A3 on L2 & A4 on L2 & A5 on L1 & A5 on L2 & A1 on L3 & A3 on L3 & A2 on L4 & A4 on L4 & not A5 on L3 & not A5 on L4 & L1 <> L2 & L3 <> L4 holds

ex A6 being POINT of (G_ (k,X)) st

( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) )

let L1, L2, L3, L4 be LINE of (G_ (k,X)); :: thesis: ( A1 on L1 & A2 on L1 & A3 on L2 & A4 on L2 & A5 on L1 & A5 on L2 & A1 on L3 & A3 on L3 & A2 on L4 & A4 on L4 & not A5 on L3 & not A5 on L4 & L1 <> L2 & L3 <> L4 implies ex A6 being POINT of (G_ (k,X)) st

( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) ) )

assume that

A5: A1 on L1 and

A6: A2 on L1 and

A7: A3 on L2 and

A8: A4 on L2 and

A9: A5 on L1 and

A10: A5 on L2 and

A11: A1 on L3 and

A12: A3 on L3 and

A13: A2 on L4 and

A14: A4 on L4 and

A15: not A5 on L3 and

A16: not A5 on L4 and

A17: L1 <> L2 and

A18: L3 <> L4 ; :: thesis: ex A6 being POINT of (G_ (k,X)) st

( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) )

A19: ( A1 c= L1 & A2 c= L1 ) by A1, A2, A5, A6, Th10;

A20: ( A3 c= L2 & A4 c= L2 ) by A1, A2, A7, A8, Th10;

A21: ( A5 c= L1 & A5 c= L2 ) by A1, A2, A9, A10, Th10;

A5 in the Points of (G_ (k,X)) ;

then A22: ex B5 being Subset of X st

( B5 = A5 & card B5 = k ) by A3;

A2 in the Points of (G_ (k,X)) ;

then A23: ex B2 being Subset of X st

( B2 = A2 & card B2 = k ) by A3;

then A24: A2 is finite ;

reconsider k1 = k - 1 as Element of NAT by A1, NAT_1:20;

L3 in the Lines of (G_ (k,X)) ;

then A25: ex K3 being Subset of X st

( K3 = L3 & card K3 = k + 1 ) by A4;

then A26: L3 is finite ;

L4 in the Lines of (G_ (k,X)) ;

then ex K4 being Subset of X st

( K4 = L4 & card K4 = k + 1 ) by A4;

then card (L3 /\ L4) in Segm (k + 1) by A25, A18, Th1;

then card (L3 /\ L4) in succ (Segm k) by NAT_1:38;

then A27: card (L3 /\ L4) c= k by ORDINAL1:22;

A1 in the Points of (G_ (k,X)) ;

then A28: ex B1 being Subset of X st

( B1 = A1 & card B1 = k ) by A3;

then A29: A1 is finite ;

G_ (k,X) is Vebleian by A1, A2, Th11;

then consider A6 being POINT of (G_ (k,X)) such that

A30: A6 on L3 and

A31: A6 on L4 by A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17;

A6 in the Points of (G_ (k,X)) ;

then A32: ex a6 being Subset of X st

( a6 = A6 & card a6 = k ) by A3;

then A33: A6 is finite ;

A34: ( A6 c= L3 & A6 c= L4 ) by A1, A2, A30, A31, Th10;

then A6 c= L3 /\ L4 by XBOOLE_1:19;

then k c= card (L3 /\ L4) by A32, CARD_1:11;

then card (L3 /\ L4) = k by A27, XBOOLE_0:def 10;

then A35: L3 /\ L4 = A6 by A32, A34, A26, CARD_2:102, XBOOLE_1:19;

L2 in the Lines of (G_ (k,X)) ;

then A36: ex K2 being Subset of X st

( K2 = L2 & card K2 = k + 1 ) by A4;

then A37: L2 is finite ;

A4 in the Points of (G_ (k,X)) ;

then A38: ex B4 being Subset of X st

( B4 = A4 & card B4 = k ) by A3;

then A39: A4 is finite ;

L1 in the Lines of (G_ (k,X)) ;

then A40: ex K1 being Subset of X st

( K1 = L1 & card K1 = k + 1 ) by A4;

then A41: L1 is finite ;

A3 in the Points of (G_ (k,X)) ;

then A42: ex B3 being Subset of X st

( B3 = A3 & card B3 = k ) by A3;

then A43: A3 is finite ;

A44: ( A3 c= L3 & A4 c= L4 ) by A1, A2, A12, A14, Th10;

then A45: A3 /\ A4 c= A6 by A35, XBOOLE_1:27;

A46: ( A1 c= L3 & A2 c= L4 ) by A1, A2, A11, A13, Th10;

then A47: A1 /\ A2 c= A6 by A35, XBOOLE_1:27;

then A48: (A1 /\ A2) \/ (A3 /\ A4) c= A6 by A45, XBOOLE_1:8;

A49: ( not A6 on L1 implies A6 = (A1 /\ A2) \/ (A3 /\ A4) )

proof

( A6 on L1 implies A6 = (A1 /\ A2) \/ (A3 /\ A4) )
assume A50:
not A6 on L1
; :: thesis: A6 = (A1 /\ A2) \/ (A3 /\ A4)

A51: ( not A6 on L2 implies A6 = (A1 /\ A2) \/ (A3 /\ A4) )

end;A51: ( not A6 on L2 implies A6 = (A1 /\ A2) \/ (A3 /\ A4) )

proof

( A6 on L2 implies A6 = (A1 /\ A2) \/ (A3 /\ A4) )
A52:
A1 \/ A2 c= L1
by A19, XBOOLE_1:8;

then A53: card (A1 \/ A2) c= k + 1 by A40, CARD_1:11;

A54: A3 \/ A4 c= L2 by A20, XBOOLE_1:8;

then A55: card (A3 \/ A4) c= k + 1 by A36, CARD_1:11;

A56: card A3 = (k - 1) + 1 by A42;

card ((A1 /\ A2) \/ (A3 /\ A4)) c= k by A32, A48, CARD_1:11;

then card ((A1 /\ A2) \/ (A3 /\ A4)) in succ k by ORDINAL1:22;

then ( card ((A1 /\ A2) \/ (A3 /\ A4)) in Segm (k1 + 1) or card ((A1 /\ A2) \/ (A3 /\ A4)) = k ) by ORDINAL1:8;

then ( card ((A1 /\ A2) \/ (A3 /\ A4)) in succ (Segm k1) or card ((A1 /\ A2) \/ (A3 /\ A4)) = k ) by NAT_1:38;

then A57: ( card ((A1 /\ A2) \/ (A3 /\ A4)) c= Segm k1 or card ((A1 /\ A2) \/ (A3 /\ A4)) = k ) by ORDINAL1:22;

A58: card A1 = (k - 1) + 1 by A28;

assume A59: not A6 on L2 ; :: thesis: A6 = (A1 /\ A2) \/ (A3 /\ A4)

A60: ( A1 <> A2 & A3 <> A4 )

then card (A1 \/ A2) = k1 + (2 * 1) by A53, XBOOLE_0:def 10;

then A61: card (A1 /\ A2) = k1 by A23, A58, Th2;

k + 1 c= card (A3 \/ A4) by A42, A38, A60, Th1;

then card (A3 \/ A4) = k1 + (2 * 1) by A55, XBOOLE_0:def 10;

then A62: card (A3 /\ A4) = k1 by A38, A56, Th2;

A63: not card ((A1 /\ A2) \/ (A3 /\ A4)) = k - 1

then card ((A1 /\ A2) \/ (A3 /\ A4)) = k by A57, A63, XBOOLE_0:def 10;

hence A6 = (A1 /\ A2) \/ (A3 /\ A4) by A32, A33, A47, A45, CARD_2:102, XBOOLE_1:8; :: thesis: verum

end;then A53: card (A1 \/ A2) c= k + 1 by A40, CARD_1:11;

A54: A3 \/ A4 c= L2 by A20, XBOOLE_1:8;

then A55: card (A3 \/ A4) c= k + 1 by A36, CARD_1:11;

A56: card A3 = (k - 1) + 1 by A42;

card ((A1 /\ A2) \/ (A3 /\ A4)) c= k by A32, A48, CARD_1:11;

then card ((A1 /\ A2) \/ (A3 /\ A4)) in succ k by ORDINAL1:22;

then ( card ((A1 /\ A2) \/ (A3 /\ A4)) in Segm (k1 + 1) or card ((A1 /\ A2) \/ (A3 /\ A4)) = k ) by ORDINAL1:8;

then ( card ((A1 /\ A2) \/ (A3 /\ A4)) in succ (Segm k1) or card ((A1 /\ A2) \/ (A3 /\ A4)) = k ) by NAT_1:38;

then A57: ( card ((A1 /\ A2) \/ (A3 /\ A4)) c= Segm k1 or card ((A1 /\ A2) \/ (A3 /\ A4)) = k ) by ORDINAL1:22;

A58: card A1 = (k - 1) + 1 by A28;

assume A59: not A6 on L2 ; :: thesis: A6 = (A1 /\ A2) \/ (A3 /\ A4)

A60: ( A1 <> A2 & A3 <> A4 )

proof

then
k + 1 c= card (A1 \/ A2)
by A28, A23, Th1;
assume
( A1 = A2 or A3 = A4 )
; :: thesis: contradiction

then ( ( {A1,A6} on L3 & {A1,A6} on L4 ) or ( {A3,A6} on L3 & {A3,A6} on L4 ) ) by A11, A12, A13, A14, A30, A31, INCSP_1:1;

hence contradiction by A5, A7, A18, A50, A59, INCSP_1:def 10; :: thesis: verum

end;then ( ( {A1,A6} on L3 & {A1,A6} on L4 ) or ( {A3,A6} on L3 & {A3,A6} on L4 ) ) by A11, A12, A13, A14, A30, A31, INCSP_1:1;

hence contradiction by A5, A7, A18, A50, A59, INCSP_1:def 10; :: thesis: verum

then card (A1 \/ A2) = k1 + (2 * 1) by A53, XBOOLE_0:def 10;

then A61: card (A1 /\ A2) = k1 by A23, A58, Th2;

k + 1 c= card (A3 \/ A4) by A42, A38, A60, Th1;

then card (A3 \/ A4) = k1 + (2 * 1) by A55, XBOOLE_0:def 10;

then A62: card (A3 /\ A4) = k1 by A38, A56, Th2;

A63: not card ((A1 /\ A2) \/ (A3 /\ A4)) = k - 1

proof

k - 1 c= card ((A1 /\ A2) \/ (A3 /\ A4))
by A61, CARD_1:11, XBOOLE_1:7;
A64:
A5 c= L1 /\ L2
by A21, XBOOLE_1:19;

A65: (A1 /\ A2) /\ (A3 /\ A4) c= A1 /\ A2 by XBOOLE_1:17;

A66: ((A1 /\ A2) /\ A3) /\ A4 = (A1 /\ A2) /\ (A3 /\ A4) by XBOOLE_1:16;

A67: A1 /\ A2 c= A1 by XBOOLE_1:17;

then A68: A1 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A1 \ (((A1 /\ A2) /\ A3) /\ A4)) by A65, A66, XBOOLE_1:1, XBOOLE_1:45;

assume A69: card ((A1 /\ A2) \/ (A3 /\ A4)) = k - 1 ; :: thesis: contradiction

then card ((A1 /\ A2) \/ (A3 /\ A4)) = k1 + (2 * 0) ;

then A70: card ((A1 /\ A2) /\ (A3 /\ A4)) = k1 by A61, A62, Th2;

then A71: (A1 /\ A2) /\ (A3 /\ A4) = (A1 /\ A2) \/ (A3 /\ A4) by A29, A43, A69, CARD_2:102, XBOOLE_1:29;

then card (A1 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A28, A29, A69, A67, A65, A66, CARD_2:44, XBOOLE_1:1;

then consider x1 being object such that

A72: A1 \ (((A1 /\ A2) /\ A3) /\ A4) = {x1} by CARD_2:42;

A73: A1 /\ A2 c= A2 by XBOOLE_1:17;

then A74: A2 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A2 \ (((A1 /\ A2) /\ A3) /\ A4)) by A65, A66, XBOOLE_1:1, XBOOLE_1:45;

card (A2 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A23, A24, A69, A73, A65, A71, A66, CARD_2:44, XBOOLE_1:1;

then consider x2 being object such that

A75: A2 \ (((A1 /\ A2) /\ A3) /\ A4) = {x2} by CARD_2:42;

x1 in {x1} by TARSKI:def 1;

then A76: not x1 in ((A1 /\ A2) /\ A3) /\ A4 by A72, XBOOLE_0:def 5;

A77: (A1 /\ A2) /\ (A3 /\ A4) c= A3 /\ A4 by XBOOLE_1:17;

A78: A3 /\ A4 c= A4 by XBOOLE_1:17;

then A79: A4 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A4 \ (((A1 /\ A2) /\ A3) /\ A4)) by A77, A66, XBOOLE_1:1, XBOOLE_1:45;

card (A4 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A38, A39, A69, A78, A77, A71, A66, CARD_2:44, XBOOLE_1:1;

then consider x4 being object such that

A80: A4 \ (((A1 /\ A2) /\ A3) /\ A4) = {x4} by CARD_2:42;

A81: A3 /\ A4 c= A3 by XBOOLE_1:17;

then A82: A3 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A3 \ (((A1 /\ A2) /\ A3) /\ A4)) by A77, A66, XBOOLE_1:1, XBOOLE_1:45;

card (A3 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A42, A43, A69, A81, A77, A71, A66, CARD_2:44, XBOOLE_1:1;

then consider x3 being object such that

A83: A3 \ (((A1 /\ A2) /\ A3) /\ A4) = {x3} by CARD_2:42;

( k + 1 c= card (A3 \/ A4) & card (A3 \/ A4) c= k + 1 ) by A42, A38, A36, A60, A54, Th1, CARD_1:11;

then card (A3 \/ A4) = k + 1 by XBOOLE_0:def 10;

then A3 \/ A4 = L2 by A36, A20, A37, CARD_2:102, XBOOLE_1:8;

then A84: L2 = (((A1 /\ A2) /\ A3) /\ A4) \/ ({x3} \/ {x4}) by A83, A80, A82, A79, XBOOLE_1:5;

then A85: L2 = (((A1 /\ A2) /\ A3) /\ A4) \/ {x3,x4} by ENUMSET1:1;

A86: ( x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 )

then A87: not x2 in ((A1 /\ A2) /\ A3) /\ A4 by A75, XBOOLE_0:def 5;

( k + 1 c= card (A1 \/ A2) & card (A1 \/ A2) c= k + 1 ) by A28, A23, A40, A60, A52, Th1, CARD_1:11;

then card (A1 \/ A2) = k + 1 by XBOOLE_0:def 10;

then A1 \/ A2 = L1 by A40, A19, A41, CARD_2:102, XBOOLE_1:8;

then A88: L1 = (((A1 /\ A2) /\ A3) /\ A4) \/ ({x1} \/ {x2}) by A72, A75, A68, A74, XBOOLE_1:5;

then A89: L1 = (((A1 /\ A2) /\ A3) /\ A4) \/ {x1,x2} by ENUMSET1:1;

A90: L1 /\ L2 c= ((A1 /\ A2) /\ A3) /\ A4

((A1 /\ A2) /\ A3) /\ A4 c= L1 by A88, XBOOLE_1:10;

then ((A1 /\ A2) /\ A3) /\ A4 c= L1 /\ L2 by A94, XBOOLE_1:19;

then L1 /\ L2 = ((A1 /\ A2) /\ A3) /\ A4 by A90, XBOOLE_0:def 10;

then card (Segm k) c= card (Segm k1) by A22, A70, A66, A64, CARD_1:11;

then A95: k <= k1 by NAT_1:40;

k1 <= k1 + 1 by NAT_1:11;

then k = k - 1 by A95, XXREAL_0:1;

hence contradiction ; :: thesis: verum

end;A65: (A1 /\ A2) /\ (A3 /\ A4) c= A1 /\ A2 by XBOOLE_1:17;

A66: ((A1 /\ A2) /\ A3) /\ A4 = (A1 /\ A2) /\ (A3 /\ A4) by XBOOLE_1:16;

A67: A1 /\ A2 c= A1 by XBOOLE_1:17;

then A68: A1 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A1 \ (((A1 /\ A2) /\ A3) /\ A4)) by A65, A66, XBOOLE_1:1, XBOOLE_1:45;

assume A69: card ((A1 /\ A2) \/ (A3 /\ A4)) = k - 1 ; :: thesis: contradiction

then card ((A1 /\ A2) \/ (A3 /\ A4)) = k1 + (2 * 0) ;

then A70: card ((A1 /\ A2) /\ (A3 /\ A4)) = k1 by A61, A62, Th2;

then A71: (A1 /\ A2) /\ (A3 /\ A4) = (A1 /\ A2) \/ (A3 /\ A4) by A29, A43, A69, CARD_2:102, XBOOLE_1:29;

then card (A1 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A28, A29, A69, A67, A65, A66, CARD_2:44, XBOOLE_1:1;

then consider x1 being object such that

A72: A1 \ (((A1 /\ A2) /\ A3) /\ A4) = {x1} by CARD_2:42;

A73: A1 /\ A2 c= A2 by XBOOLE_1:17;

then A74: A2 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A2 \ (((A1 /\ A2) /\ A3) /\ A4)) by A65, A66, XBOOLE_1:1, XBOOLE_1:45;

card (A2 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A23, A24, A69, A73, A65, A71, A66, CARD_2:44, XBOOLE_1:1;

then consider x2 being object such that

A75: A2 \ (((A1 /\ A2) /\ A3) /\ A4) = {x2} by CARD_2:42;

x1 in {x1} by TARSKI:def 1;

then A76: not x1 in ((A1 /\ A2) /\ A3) /\ A4 by A72, XBOOLE_0:def 5;

A77: (A1 /\ A2) /\ (A3 /\ A4) c= A3 /\ A4 by XBOOLE_1:17;

A78: A3 /\ A4 c= A4 by XBOOLE_1:17;

then A79: A4 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A4 \ (((A1 /\ A2) /\ A3) /\ A4)) by A77, A66, XBOOLE_1:1, XBOOLE_1:45;

card (A4 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A38, A39, A69, A78, A77, A71, A66, CARD_2:44, XBOOLE_1:1;

then consider x4 being object such that

A80: A4 \ (((A1 /\ A2) /\ A3) /\ A4) = {x4} by CARD_2:42;

A81: A3 /\ A4 c= A3 by XBOOLE_1:17;

then A82: A3 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A3 \ (((A1 /\ A2) /\ A3) /\ A4)) by A77, A66, XBOOLE_1:1, XBOOLE_1:45;

card (A3 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A42, A43, A69, A81, A77, A71, A66, CARD_2:44, XBOOLE_1:1;

then consider x3 being object such that

A83: A3 \ (((A1 /\ A2) /\ A3) /\ A4) = {x3} by CARD_2:42;

( k + 1 c= card (A3 \/ A4) & card (A3 \/ A4) c= k + 1 ) by A42, A38, A36, A60, A54, Th1, CARD_1:11;

then card (A3 \/ A4) = k + 1 by XBOOLE_0:def 10;

then A3 \/ A4 = L2 by A36, A20, A37, CARD_2:102, XBOOLE_1:8;

then A84: L2 = (((A1 /\ A2) /\ A3) /\ A4) \/ ({x3} \/ {x4}) by A83, A80, A82, A79, XBOOLE_1:5;

then A85: L2 = (((A1 /\ A2) /\ A3) /\ A4) \/ {x3,x4} by ENUMSET1:1;

A86: ( x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 )

proof

x2 in {x2}
by TARSKI:def 1;
assume
( x1 = x3 or x1 = x4 or x2 = x3 or x2 = x4 )
; :: thesis: contradiction

then ( ( {A1,A5} on L1 & {A1,A5} on L2 ) or ( {A1,A5} on L1 & {A1,A5} on L2 ) or ( {A2,A5} on L1 & {A2,A5} on L2 ) or ( {A2,A5} on L1 & {A2,A5} on L2 ) ) by A5, A6, A7, A8, A9, A10, A72, A75, A83, A80, A68, A74, A82, A79, INCSP_1:1;

hence contradiction by A11, A13, A15, A16, A17, INCSP_1:def 10; :: thesis: verum

end;then ( ( {A1,A5} on L1 & {A1,A5} on L2 ) or ( {A1,A5} on L1 & {A1,A5} on L2 ) or ( {A2,A5} on L1 & {A2,A5} on L2 ) or ( {A2,A5} on L1 & {A2,A5} on L2 ) ) by A5, A6, A7, A8, A9, A10, A72, A75, A83, A80, A68, A74, A82, A79, INCSP_1:1;

hence contradiction by A11, A13, A15, A16, A17, INCSP_1:def 10; :: thesis: verum

then A87: not x2 in ((A1 /\ A2) /\ A3) /\ A4 by A75, XBOOLE_0:def 5;

( k + 1 c= card (A1 \/ A2) & card (A1 \/ A2) c= k + 1 ) by A28, A23, A40, A60, A52, Th1, CARD_1:11;

then card (A1 \/ A2) = k + 1 by XBOOLE_0:def 10;

then A1 \/ A2 = L1 by A40, A19, A41, CARD_2:102, XBOOLE_1:8;

then A88: L1 = (((A1 /\ A2) /\ A3) /\ A4) \/ ({x1} \/ {x2}) by A72, A75, A68, A74, XBOOLE_1:5;

then A89: L1 = (((A1 /\ A2) /\ A3) /\ A4) \/ {x1,x2} by ENUMSET1:1;

A90: L1 /\ L2 c= ((A1 /\ A2) /\ A3) /\ A4

proof

A94:
((A1 /\ A2) /\ A3) /\ A4 c= L2
by A84, XBOOLE_1:10;
assume
not L1 /\ L2 c= ((A1 /\ A2) /\ A3) /\ A4
; :: thesis: contradiction

then consider x being object such that

A91: x in L1 /\ L2 and

A92: not x in ((A1 /\ A2) /\ A3) /\ A4 ;

x in L1 by A91, XBOOLE_0:def 4;

then A93: x in {x1,x2} by A89, A92, XBOOLE_0:def 3;

x in L2 by A91, XBOOLE_0:def 4;

then ( x1 in L2 or x2 in L2 ) by A93, TARSKI:def 2;

then ( x1 in {x3,x4} or x2 in {x3,x4} ) by A85, A76, A87, XBOOLE_0:def 3;

hence contradiction by A86, TARSKI:def 2; :: thesis: verum

end;then consider x being object such that

A91: x in L1 /\ L2 and

A92: not x in ((A1 /\ A2) /\ A3) /\ A4 ;

x in L1 by A91, XBOOLE_0:def 4;

then A93: x in {x1,x2} by A89, A92, XBOOLE_0:def 3;

x in L2 by A91, XBOOLE_0:def 4;

then ( x1 in L2 or x2 in L2 ) by A93, TARSKI:def 2;

then ( x1 in {x3,x4} or x2 in {x3,x4} ) by A85, A76, A87, XBOOLE_0:def 3;

hence contradiction by A86, TARSKI:def 2; :: thesis: verum

((A1 /\ A2) /\ A3) /\ A4 c= L1 by A88, XBOOLE_1:10;

then ((A1 /\ A2) /\ A3) /\ A4 c= L1 /\ L2 by A94, XBOOLE_1:19;

then L1 /\ L2 = ((A1 /\ A2) /\ A3) /\ A4 by A90, XBOOLE_0:def 10;

then card (Segm k) c= card (Segm k1) by A22, A70, A66, A64, CARD_1:11;

then A95: k <= k1 by NAT_1:40;

k1 <= k1 + 1 by NAT_1:11;

then k = k - 1 by A95, XXREAL_0:1;

hence contradiction ; :: thesis: verum

then card ((A1 /\ A2) \/ (A3 /\ A4)) = k by A57, A63, XBOOLE_0:def 10;

hence A6 = (A1 /\ A2) \/ (A3 /\ A4) by A32, A33, A47, A45, CARD_2:102, XBOOLE_1:8; :: thesis: verum

proof

hence
A6 = (A1 /\ A2) \/ (A3 /\ A4)
by A51; :: thesis: verum
assume A96:
A6 on L2
; :: thesis: A6 = (A1 /\ A2) \/ (A3 /\ A4)

A97: A4 = A6

end;A97: A4 = A6

proof

A3 = A6
assume A98:
A4 <> A6
; :: thesis: contradiction

( {A4,A6} on L2 & {A4,A6} on L4 ) by A8, A14, A31, A96, INCSP_1:1;

hence contradiction by A10, A16, A98, INCSP_1:def 10; :: thesis: verum

end;( {A4,A6} on L2 & {A4,A6} on L4 ) by A8, A14, A31, A96, INCSP_1:1;

hence contradiction by A10, A16, A98, INCSP_1:def 10; :: thesis: verum

proof

hence
A6 = (A1 /\ A2) \/ (A3 /\ A4)
by A46, A35, A97, XBOOLE_1:12, XBOOLE_1:27; :: thesis: verum
assume A99:
A3 <> A6
; :: thesis: contradiction

( {A3,A6} on L2 & {A3,A6} on L3 ) by A7, A12, A30, A96, INCSP_1:1;

hence contradiction by A10, A15, A99, INCSP_1:def 10; :: thesis: verum

end;( {A3,A6} on L2 & {A3,A6} on L3 ) by A7, A12, A30, A96, INCSP_1:1;

hence contradiction by A10, A15, A99, INCSP_1:def 10; :: thesis: verum

proof

hence
ex A6 being POINT of (G_ (k,X)) st
assume A100:
A6 on L1
; :: thesis: A6 = (A1 /\ A2) \/ (A3 /\ A4)

A101: A1 = A6

end;A101: A1 = A6

proof

A2 = A6
assume A102:
A1 <> A6
; :: thesis: contradiction

( {A1,A6} on L1 & {A1,A6} on L3 ) by A5, A11, A30, A100, INCSP_1:1;

hence contradiction by A9, A15, A102, INCSP_1:def 10; :: thesis: verum

end;( {A1,A6} on L1 & {A1,A6} on L3 ) by A5, A11, A30, A100, INCSP_1:1;

hence contradiction by A9, A15, A102, INCSP_1:def 10; :: thesis: verum

proof

hence
A6 = (A1 /\ A2) \/ (A3 /\ A4)
by A44, A35, A101, XBOOLE_1:12, XBOOLE_1:27; :: thesis: verum
assume A103:
A2 <> A6
; :: thesis: contradiction

( {A2,A6} on L1 & {A2,A6} on L4 ) by A6, A13, A31, A100, INCSP_1:1;

hence contradiction by A9, A16, A103, INCSP_1:def 10; :: thesis: verum

end;( {A2,A6} on L1 & {A2,A6} on L4 ) by A6, A13, A31, A100, INCSP_1:1;

hence contradiction by A9, A16, A103, INCSP_1:def 10; :: thesis: verum

( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) ) by A30, A31, A49; :: thesis: verum