:: ANPROJ_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: ANPROJ_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, w being Element of V st ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) holds
( u is_Prop_Vect & v is_Prop_Vect & w is_Prop_Vect & not u,v,w are_LinDep & not are_Prop u,v )
proof end;

Lm1: for V being RealLinearSpace
for u, v being Element of V st ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) holds
( u is_Prop_Vect & v is_Prop_Vect & not are_Prop u,v )
proof end;

theorem Th2: :: ANPROJ_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, u1, v1 being Element of V st ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) holds
( u is_Prop_Vect & v is_Prop_Vect & not are_Prop u,v & u1 is_Prop_Vect & v1 is_Prop_Vect & not are_Prop u1,v1 & not u,v,u1 are_LinDep & not u1,v1,u are_LinDep )
proof end;

Lm2: for V being RealLinearSpace
for v, w, u being Element of V
for a, b, c, d being Real holds a * (((b * v) + (c * w)) + (d * u)) = (((a * b) * v) + ((a * c) * w)) + ((a * d) * u)
proof end;

Lm3: for V being RealLinearSpace
for u, v, w, u1, v1, w1 being Element of V holds ((u + v) + w) + ((u1 + v1) + w1) = ((u + u1) + (v + v1)) + (w + w1)
proof end;

theorem Th3: :: ANPROJ_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for p, q, r being Element of V st ( for w being Element of V ex a, b, c being Real st w = ((a * p) + (b * q)) + (c * r) ) & ( for a, b, c being Real st ((a * p) + (b * q)) + (c * r) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) holds
for u, u1 being Element of V ex y being Element of V st
( p,q,y are_LinDep & u,u1,y are_LinDep & y is_Prop_Vect )
proof end;

Lm4: for V being RealLinearSpace
for v, w, u, y being Element of V
for a, b, c, d, d1 being Real holds a * ((((b * v) + (c * w)) + (d * u)) + (d1 * y)) = ((((a * b) * v) + ((a * c) * w)) + ((a * d) * u)) + ((a * d1) * y)
proof end;

Lm5: for V being RealLinearSpace
for u, v, w, y, u1, v1, w1, y1 being Element of V holds (((u + v) + w) + y) + (((u1 + v1) + w1) + y1) = (((u + u1) + (v + v1)) + (w + w1)) + (y + y1)
proof end;

Lm6: for V being RealLinearSpace
for v, w, u being Element of V
for a, b, c, d being Real holds a * (((b * v) + (c * w)) + (d * u)) = (((a * b) * v) + ((a * c) * w)) + ((a * d) * u)
proof end;

Lm7: for V being RealLinearSpace
for y, p, w, q, r being Element of V
for a1, b1, a, b, c being Real st y = (a1 * p) + (b1 * w) & w = ((a * p) + (b * q)) + (c * r) holds
y = (((a1 + (b1 * a)) * p) + ((b1 * b) * q)) + ((b1 * c) * r)
proof end;

theorem Th4: :: ANPROJ_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for p, q, r, s being Element of V st ( for w being Element of V ex a, b, c, d being Real st w = (((a * p) + (b * q)) + (c * r)) + (d * s) ) & ( for a, b, c, d being Real st (((a * p) + (b * q)) + (c * r)) + (d * s) = 0. V holds
( a = 0 & b = 0 & c = 0 & d = 0 ) ) holds
for u, v being Element of V st u is_Prop_Vect & v is_Prop_Vect holds
ex y, w being Element of V st
( u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & y is_Prop_Vect & w is_Prop_Vect )
proof end;

theorem Th5: :: ANPROJ_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, u1, v1 being Element of V st ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) holds
for y being Element of V holds
( not y is_Prop_Vect or not u,v,y are_LinDep or not u1,v1,y are_LinDep )
proof end;

definition
let V be RealLinearSpace;
let u, v, w be Element of V;
pred u,v,w are_Prop_Vect means :Def1: :: ANPROJ_2:def 1
( u is_Prop_Vect & v is_Prop_Vect & w is_Prop_Vect );
end;

:: deftheorem Def1 defines are_Prop_Vect ANPROJ_2:def 1 :
for V being RealLinearSpace
for u, v, w being Element of V holds
( u,v,w are_Prop_Vect iff ( u is_Prop_Vect & v is_Prop_Vect & w is_Prop_Vect ) );

definition
let V be RealLinearSpace;
let u, v, w, u1, v1, w1 be Element of V;
pred u,v,w,u1,v1,w1 lie_on_a_triangle means :Def2: :: ANPROJ_2:def 2
( u,v,w1 are_LinDep & u,w,v1 are_LinDep & v,w,u1 are_LinDep );
end;

:: deftheorem Def2 defines lie_on_a_triangle ANPROJ_2:def 2 :
for V being RealLinearSpace
for u, v, w, u1, v1, w1 being Element of V holds
( u,v,w,u1,v1,w1 lie_on_a_triangle iff ( u,v,w1 are_LinDep & u,w,v1 are_LinDep & v,w,u1 are_LinDep ) );

definition
let V be RealLinearSpace;
let o, u, v, w, u2, v2, w2 be Element of V;
pred o,u,v,w,u2,v2,w2 are_perspective means :Def3: :: ANPROJ_2:def 3
( o,u,u2 are_LinDep & o,v,v2 are_LinDep & o,w,w2 are_LinDep );
end;

:: deftheorem Def3 defines are_perspective ANPROJ_2:def 3 :
for V being RealLinearSpace
for o, u, v, w, u2, v2, w2 being Element of V holds
( o,u,v,w,u2,v2,w2 are_perspective iff ( o,u,u2 are_LinDep & o,v,v2 are_LinDep & o,w,w2 are_LinDep ) );

Lm8: for V being RealLinearSpace
for o being Element of V
for a being Real holds - (a * o) = (- a) * o
proof end;

theorem Th6: :: ANPROJ_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for o, u, u2 being Element of V st o,u,u2 are_LinDep & not are_Prop o,u & not are_Prop o,u2 & not are_Prop u,u2 & o,u,u2 are_Prop_Vect holds
( ex a1, b1 being Real st
( b1 * u2 = o + (a1 * u) & a1 <> 0 & b1 <> 0 ) & ex a2, c2 being Real st
( u2 = (c2 * o) + (a2 * u) & c2 <> 0 & a2 <> 0 ) )
proof end;

theorem Th7: :: ANPROJ_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for p, q, r being Element of V st p,q,r are_LinDep & not are_Prop p,q & p,q,r are_Prop_Vect holds
ex a, b being Real st r = (a * p) + (b * q)
proof end;

Lm9: for V being RealLinearSpace
for u2, w2 being Element of V
for b1 being Real st b1 * u2 = w2 & b1 <> 0 holds
are_Prop u2,w2
proof end;

Lm10: for V being RealLinearSpace
for q, o, p, r, s being Element of V
for a, b being Real st q = o + (a * p) & r = o + (b * s) & are_Prop q,r & a <> 0 holds
o,p,s are_LinDep
proof end;

Lm11: for V being RealLinearSpace
for p, q being Element of V
for a being Real st a * p = q & a <> 0 & p is_Prop_Vect holds
q is_Prop_Vect
proof end;

Lm12: for V being RealLinearSpace
for r, u2, v2, o, u, v being Element of V
for a1, a2, A, B being Real st r = (A * u2) + (B * v2) & u2 = o + (a1 * u) & v2 = o + (a2 * v) holds
r = (((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v)
proof end;

Lm13: for V being RealLinearSpace
for r, p, q, o being Element of V
for a, b being Real st r = (a * p) + (b * q) holds
r = ((0 * o) + (a * p)) + (b * q)
proof end;

Lm14: for V being RealLinearSpace
for p, q being Element of V holds (0 * p) + (0 * q) = 0. V
proof end;

Lm15: for V being RealLinearSpace
for o, v, w being Element of V
for b, a2, a3 being Real holds ((0 * o) + ((b * a2) * v)) + (((- b) * a3) * w) = b * ((a2 * v) - (a3 * w))
proof end;

theorem Th8: :: ANPROJ_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for o, u, v, w, u2, v2, w2, u1, v1, w1 being Element of V st o is_Prop_Vect & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 are_perspective & not are_Prop o,u2 & not are_Prop o,v2 & not are_Prop o,w2 & not are_Prop u,u2 & not are_Prop v,v2 & not are_Prop w,w2 & not o,u,v are_LinDep & not o,u,w are_LinDep & not o,v,w are_LinDep & u,v,w,u1,v1,w1 lie_on_a_triangle & u2,v2,w2,u1,v1,w1 lie_on_a_triangle holds
u1,v1,w1 are_LinDep
proof end;

definition
let V be RealLinearSpace;
let o, u, v, w, u2, v2, w2 be Element of V;
pred o,u,v,w,u2,v2,w2 lie_on_an_angle means :Def4: :: ANPROJ_2:def 4
( not o,u,u2 are_LinDep & o,u,v are_LinDep & o,u,w are_LinDep & o,u2,v2 are_LinDep & o,u2,w2 are_LinDep );
end;

:: deftheorem Def4 defines lie_on_an_angle ANPROJ_2:def 4 :
for V being RealLinearSpace
for o, u, v, w, u2, v2, w2 being Element of V holds
( o,u,v,w,u2,v2,w2 lie_on_an_angle iff ( not o,u,u2 are_LinDep & o,u,v are_LinDep & o,u,w are_LinDep & o,u2,v2 are_LinDep & o,u2,w2 are_LinDep ) );

definition
let V be RealLinearSpace;
let o, u, v, w, u2, v2, w2 be Element of V;
pred o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop means :Def5: :: ANPROJ_2:def 5
( not are_Prop o,v & not are_Prop o,w & not are_Prop o,v2 & not are_Prop o,w2 & not are_Prop u,v & not are_Prop u,w & not are_Prop u2,v2 & not are_Prop u2,w2 & not are_Prop v,w & not are_Prop v2,w2 );
end;

:: deftheorem Def5 defines are_half_mutually_not_Prop ANPROJ_2:def 5 :
for V being RealLinearSpace
for o, u, v, w, u2, v2, w2 being Element of V holds
( o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop iff ( not are_Prop o,v & not are_Prop o,w & not are_Prop o,v2 & not are_Prop o,w2 & not are_Prop u,v & not are_Prop u,w & not are_Prop u2,v2 & not are_Prop u2,w2 & not are_Prop v,w & not are_Prop v2,w2 ) );

Lm16: for V being RealLinearSpace
for u2, w2 being Element of V
for b1 being Real st b1 * u2 = w2 & b1 <> 0 holds
are_Prop u2,w2
proof end;

Lm17: for V being RealLinearSpace
for p, q, y being Element of V
for a being Real st not are_Prop p,q & y = a * q & a <> 0 holds
not are_Prop p,y
proof end;

Lm18: for V being RealLinearSpace
for w1, u, v2, o, u2 being Element of V
for a, b, c2 being Real st w1 = (a * u) + (b * v2) & v2 = o + (c2 * u2) holds
w1 = ((b * o) + (a * u)) + ((b * c2) * u2)
proof end;

Lm19: for V being RealLinearSpace
for w1, u2, v1, o, u being Element of V
for a, b, a2 being Real st w1 = (a * u2) + (b * v1) & v1 = o + (a2 * u) holds
w1 = ((b * o) + ((b * a2) * u)) + (a * u2)
proof end;

Lm20: for V being RealLinearSpace
for p, q being Element of V
for a being Real st a * p = q & a <> 0 & p is_Prop_Vect holds
q is_Prop_Vect
proof end;

Lm21: for V being RealLinearSpace
for p, q, y, s being Element of V
for a, b being Real st not are_Prop p,q & y = a * q & a <> 0 & s = b * p & b <> 0 holds
not are_Prop s,y
proof end;

Lm22: for V being RealLinearSpace
for r, u2, v2, o, u, v being Element of V
for a1, a2, A, B being Real st r = (A * u2) + (B * v2) & u2 = o + (a1 * u) & v2 = o + (a2 * v) holds
r = (((A + B) * o) + ((A * a1) * u)) + ((B * a2) * v)
proof end;

Lm23: for a2, a3, c2 being Real st a2 <> a3 & c2 <> 0 holds
(a3 * c2) - (a2 * c2) <> 0
proof end;

Lm24: for a2, a3, c3, c2, A1, A1', B1, B1' being Real st A1 + B1 = A1' + B1' & A1 * a2 = A1' * a3 & B1 * c3 = B1' * c2 & a2 <> a3 & c2 <> 0 holds
A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) " )) * B1
proof end;

Lm25: for c2, a2, a3, B1 being Real st c2 <> 0 & a2 <> a3 & B1 <> 0 holds
B1 * (((a3 * c2) - (a2 * c2)) " ) <> 0
proof end;

Lm26: for V being RealLinearSpace
for u1, o, u, u2 being Element of V
for a3, c3, c2, a2, A1, B1 being Real st A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) " )) * B1 & c2 <> 0 & a2 <> a3 & u1 = (((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2) holds
u1 = (B1 * (((a3 * c2) - (a2 * c2)) " )) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))
proof end;

Lm27: for V being RealLinearSpace
for p, q, r, u, u2, u1 being Element of V holds ((p + q) + r) + ((u + u2) + u1) = ((p + u) + (q + u2)) + (r + u1)
proof end;

Lm28: for V being RealLinearSpace
for u1, o, u, u2, v1, w2 being Element of V
for a3, c3, a2, c2, C2, C3 being Real st u1 = ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2) & v1 = (o + (a3 * u)) + (c3 * u2) & w2 = (o + (a2 * u)) + (c2 * u2) & C2 + C3 = (a2 * c2) - (a3 * c3) & (C2 * a3) + (C3 * a2) = (a2 * a3) * (c2 - c3) & (C2 * c3) + (C3 * c2) = (c2 * c3) * (a2 - a3) holds
((1 * u1) + (C2 * v1)) + (C3 * w2) = 0. V
proof end;

Lm29: for V being RealLinearSpace
for w2, o, u, u2, w1 being Element of V
for a2, c2, A3, A3', B3, B3' being Real st w2 = (o + (a2 * u)) + (c2 * u2) & w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) & B3 = B3' & A3 = B3' * a2 & B3 * c2 = A3' holds
w1 = B3 * w2
proof end;

theorem Th9: :: ANPROJ_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for o, u, v, w, u2, v2, w2, u1, v1, w1 being Element of V st o is_Prop_Vect & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 lie_on_an_angle & o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop & u,v2,w1 are_LinDep & u2,v,w1 are_LinDep & u,w2,v1 are_LinDep & w,u2,v1 are_LinDep & v,w2,u1 are_LinDep & w,v2,u1 are_LinDep holds
u1,v1,w1 are_LinDep
proof end;

theorem Th10: :: ANPROJ_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for x1, x2, x3 being Element of A ex f, g, h being Element of Funcs A,REAL st
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x2 implies g . z = 1 ) & ( z <> x2 implies g . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x3 implies h . z = 1 ) & ( z <> x3 implies h . z = 0 ) ) ) )
proof end;

theorem Th11: :: ANPROJ_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f, g, h being Element of Funcs A,REAL
for x1, x2, x3 being Element of A st x1 in A & x2 in A & x3 in A & x1 <> x2 & x1 <> x3 & x2 <> x3 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x2 implies g . z = 1 ) & ( z <> x2 implies g . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x3 implies h . z = 1 ) & ( z <> x3 implies h . z = 0 ) ) ) holds
for a, b, c being Real st (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h]) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 )
proof end;

theorem :: ANPROJ_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for x1, x2, x3 being Element of A st x1 in A & x2 in A & x3 in A & x1 <> x2 & x1 <> x3 & x2 <> x3 holds
ex f, g, h being Element of Funcs A,REAL st
for a, b, c being Real st (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h]) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 )
proof end;

theorem Th13: :: ANPROJ_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f, g, h being Element of Funcs A,REAL
for x1, x2, x3 being Element of A st A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x2 implies g . z = 1 ) & ( z <> x2 implies g . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x3 implies h . z = 1 ) & ( z <> x3 implies h . z = 0 ) ) ) holds
for h' being Element of Funcs A,REAL ex a, b, c being Real st h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])
proof end;

theorem :: ANPROJ_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for x1, x2, x3 being Element of A st A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 holds
ex f, g, h being Element of Funcs A,REAL st
for h' being Element of Funcs A,REAL ex a, b, c being Real st h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])
proof end;

theorem Th15: :: ANPROJ_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for x1, x2, x3 being Element of A st A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 holds
ex f, g, h being Element of Funcs A,REAL st
( ( for a, b, c being Real st (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h]) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 ) ) & ( for h' being Element of Funcs A,REAL ex a, b, c being Real st h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h]) ) )
proof end;

Lm30: ex A being non empty set ex x1, x2, x3 being Element of A st
( A = {x1,x2,x3} & x1 <> x2 & x1 <> x3 & x2 <> x3 )
proof end;

theorem Th16: :: ANPROJ_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex V being non trivial RealLinearSpace ex u, v, w being Element of V st
( ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) )
proof end;

theorem Th17: :: ANPROJ_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for x1, x2, x3, x4 being Element of A ex f, g, h, f1 being Element of Funcs A,REAL st
( ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x2 implies g . z = 1 ) & ( z <> x2 implies g . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x3 implies h . z = 1 ) & ( z <> x3 implies h . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x4 implies f1 . z = 1 ) & ( z <> x4 implies f1 . z = 0 ) ) ) )
proof end;

theorem Th18: :: ANPROJ_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f, g, h, f1 being Element of Funcs A,REAL
for x1, x2, x3, x4 being Element of A st x1 in A & x2 in A & x3 in A & x4 in A & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x2 implies g . z = 1 ) & ( z <> x2 implies g . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x3 implies h . z = 1 ) & ( z <> x3 implies h . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x4 implies f1 . z = 1 ) & ( z <> x4 implies f1 . z = 0 ) ) ) holds
for a, b, c, d being Real st (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1]) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 & d = 0 )
proof end;

theorem :: ANPROJ_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for x1, x2, x3, x4 being Element of A st x1 in A & x2 in A & x3 in A & x4 in A & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds
ex f, g, h, f1 being Element of Funcs A,REAL st
for a, b, c, d being Real st (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1]) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 & d = 0 )
proof end;

theorem Th20: :: ANPROJ_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for f, g, h, f1 being Element of Funcs A,REAL
for x1, x2, x3, x4 being Element of A st A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 & ( for z being set st z in A holds
( ( z = x1 implies f . z = 1 ) & ( z <> x1 implies f . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x2 implies g . z = 1 ) & ( z <> x2 implies g . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x3 implies h . z = 1 ) & ( z <> x3 implies h . z = 0 ) ) ) & ( for z being set st z in A holds
( ( z = x4 implies f1 . z = 1 ) & ( z <> x4 implies f1 . z = 0 ) ) ) holds
for h' being Element of Funcs A,REAL ex a, b, c, d being Real st h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1])
proof end;

theorem :: ANPROJ_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for x1, x2, x3, x4 being Element of A st A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds
ex f, g, h, f1 being Element of Funcs A,REAL st
for h' being Element of Funcs A,REAL ex a, b, c, d being Real st h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1])
proof end;

theorem Th22: :: ANPROJ_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for x1, x2, x3, x4 being Element of A st A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds
ex f, g, h, f1 being Element of Funcs A,REAL st
( ( for a, b, c, d being Real st (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1]) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for h' being Element of Funcs A,REAL ex a, b, c, d being Real st h' = (RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncAdd A) . ((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])),((RealFuncExtMult A) . [c,h])),((RealFuncExtMult A) . [d,f1]) ) )
proof end;

Lm31: ex A being non empty set ex x1, x2, x3, x4 being Element of A st
( A = {x1,x2,x3,x4} & x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 )
proof end;

theorem Th23: :: ANPROJ_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex V being non trivial RealLinearSpace ex u, v, w, u1 being Element of V st
( ( for a, b, c, d being Real st (((a * u) + (b * v)) + (c * w)) + (d * u1) = 0. V holds
( a = 0 & b = 0 & c = 0 & d = 0 ) ) & ( for y being Element of V ex a, b, c, d being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) )
proof end;

definition
let IT be RealLinearSpace;
attr IT is up-3-dimensional means :Def6: :: ANPROJ_2:def 6
 ex u, v, w1 being Element of IT st
for a, b, c being Real st ((a * u) + (b * v)) + (c * w1) = 0. IT holds
( a = 0 & b = 0 & c = 0 );
end;

:: deftheorem Def6 defines up-3-dimensional ANPROJ_2:def 6 :
for IT being RealLinearSpace holds
( IT is up-3-dimensional iff ex u, v, w1 being Element of IT st
for a, b, c being Real st ((a * u) + (b * v)) + (c * w1) = 0. IT holds
( a = 0 & b = 0 & c = 0 ) );

registration
cluster up-3-dimensional RLSStruct ;
existence
ex b1 being RealLinearSpace st b1 is up-3-dimensional
proof end;
end;

registration
cluster up-3-dimensional -> non trivial RLSStruct ;
coherence
for b1 being RealLinearSpace st b1 is up-3-dimensional holds
not b1 is trivial
proof end;
end;

definition
let CS be non empty CollStr ;
redefine attr CS is reflexive means :Def7: :: ANPROJ_2:def 7
for p, q, r being Element of CS holds
( p,q,p is_collinear & p,p,q is_collinear & p,q,q is_collinear );
compatibility
( CS is reflexive iff for p, q, r being Element of CS holds
( p,q,p is_collinear & p,p,q is_collinear & p,q,q is_collinear ) )
proof end;
redefine attr CS is transitive means :Def8: :: ANPROJ_2:def 8
for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear holds
r,r1,r2 is_collinear ;
compatibility
( CS is transitive iff for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear holds
r,r1,r2 is_collinear )
proof end;
end;

:: deftheorem Def7 defines reflexive ANPROJ_2:def 7 :
for CS being non empty CollStr holds
( CS is reflexive iff for p, q, r being Element of CS holds
( p,q,p is_collinear & p,p,q is_collinear & p,q,q is_collinear ) );

:: deftheorem Def8 defines transitive ANPROJ_2:def 8 :
for CS being non empty CollStr holds
( CS is transitive iff for p, q, r, r1, r2 being Element of CS st p <> q & p,q,r is_collinear & p,q,r1 is_collinear & p,q,r2 is_collinear holds
r,r1,r2 is_collinear );

definition
let IT be non empty CollStr ;
attr IT is Vebleian means :Def9: :: ANPROJ_2:def 9
for p, p1, p2, r, r1 being Element of IT st p,p1,r is_collinear & p1,p2,r1 is_collinear holds
ex r2 being Element of IT st
( p,p2,r2 is_collinear & r,r1,r2 is_collinear );
attr IT is at_least_3rank means :Def10: :: ANPROJ_2:def 10
for p, q being Element of IT ex r being Element of IT st
( p <> r & q <> r & p,q,r is_collinear );
end;

:: deftheorem Def9 defines Vebleian ANPROJ_2:def 9 :
for IT being non empty CollStr holds
( IT is Vebleian iff for p, p1, p2, r, r1 being Element of IT st p,p1,r is_collinear & p1,p2,r1 is_collinear holds
ex r2 being Element of IT st
( p,p2,r2 is_collinear & r,r1,r2 is_collinear ) );

:: deftheorem Def10 defines at_least_3rank ANPROJ_2:def 10 :
for IT being non empty CollStr holds
( IT is at_least_3rank iff for p, q being Element of IT ex r being Element of IT st
( p <> r & q <> r & p,q,r is_collinear ) );

theorem Th24: :: ANPROJ_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non trivial RealLinearSpace
for p, q, r being Element of (ProjectiveSpace V) holds
( p,q,r is_collinear iff ex u, v, w being Element of V st
( p = Dir u & q = Dir v & r = Dir w & u is_Prop_Vect & v is_Prop_Vect & w is_Prop_Vect & u,v,w are_LinDep ) )
proof end;

Lm32: for V being non trivial RealLinearSpace holds ProjectiveSpace V is reflexive
proof end;

Lm33: for V being non trivial RealLinearSpace holds ProjectiveSpace V is transitive
proof end;

registration
let V be non trivial RealLinearSpace;
cluster ProjectiveSpace V -> reflexive transitive ;
coherence
( ProjectiveSpace V is reflexive & ProjectiveSpace V is transitive ) by Lm32, Lm33;
end;

theorem Th25: :: ANPROJ_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non trivial RealLinearSpace
for p, q, r being Element of (ProjectiveSpace V) st p,q,r is_collinear holds
( p,r,q is_collinear & q,p,r is_collinear & r,q,p is_collinear & r,p,q is_collinear & q,r,p is_collinear )
proof end;

Lm34: for V being non trivial RealLinearSpace
for p, p1, p2, r, r1 being Element of (ProjectiveSpace V) st p,p1,p2 is_collinear & p,p1,r is_collinear & p1,p2,r1 is_collinear holds
ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 is_collinear & r,r1,r2 is_collinear )
proof end;

Lm35: for V being non trivial RealLinearSpace
for p, p1, p2, r, r1 being Element of (ProjectiveSpace V) st not p,p1,p2 is_collinear & p,p1,r is_collinear & p1,p2,r1 is_collinear holds
ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 is_collinear & r,r1,r2 is_collinear )
proof end;

Lm36: for V being non trivial RealLinearSpace holds ProjectiveSpace V is Vebleian
proof end;

registration
let V be non trivial RealLinearSpace;
cluster ProjectiveSpace V -> reflexive transitive Vebleian ;
coherence
ProjectiveSpace V is Vebleian by Lm36;
end;

Lm37: for V being non trivial RealLinearSpace st V is up-3-dimensional holds
ProjectiveSpace V is proper
proof end;

registration
let V be up-3-dimensional RealLinearSpace;
cluster ProjectiveSpace V -> reflexive transitive proper Vebleian ;
coherence
ProjectiveSpace V is proper by Lm37;
end;

theorem Th26: :: ANPROJ_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non trivial RealLinearSpace st ex u, v being Element of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) holds
ProjectiveSpace V is at_least_3rank
proof end;

Lm38: for V being non trivial RealLinearSpace st V is up-3-dimensional holds
ProjectiveSpace V is at_least_3rank
proof end;

registration
let V be up-3-dimensional RealLinearSpace;
cluster ProjectiveSpace V -> reflexive transitive proper Vebleian at_least_3rank ;
coherence
ProjectiveSpace V is at_least_3rank by Lm38;
end;

registration
cluster non empty reflexive transitive proper Vebleian at_least_3rank CollStr ;
existence
ex b1 being non empty CollStr st
( b1 is transitive & b1 is reflexive & b1 is proper & b1 is Vebleian & b1 is at_least_3rank )
proof end;
end;

definition
mode CollProjectiveSpace is non empty reflexive transitive proper Vebleian at_least_3rank CollStr ;
end;

Lm39: for V being up-3-dimensional RealLinearSpace holds ProjectiveSpace V is CollProjectiveSpace
;

definition
let IT be CollProjectiveSpace;
attr IT is Fanoian means :Def11: :: ANPROJ_2:def 11
for p1, r2, q, r1, q1, p, r being Element of IT st p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear & r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear & not p1,r2,q1 is_collinear & not p1,r2,r1 is_collinear & not p1,r1,q1 is_collinear holds
r2,r1,q1 is_collinear ;
attr IT is Desarguesian means :: ANPROJ_2:def 12
for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of IT st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 is_collinear & not o,p1,p3 is_collinear & not o,p2,p3 is_collinear & p1,p2,r3 is_collinear & q1,q2,r3 is_collinear & p2,p3,r1 is_collinear & q2,q3,r1 is_collinear & p1,p3,r2 is_collinear & q1,q3,r2 is_collinear & o,p1,q1 is_collinear & o,p2,q2 is_collinear & o,p3,q3 is_collinear holds
r1,r2,r3 is_collinear ;
attr IT is Pappian means :: ANPROJ_2:def 13
for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of IT st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 is_collinear & o,p1,p2 is_collinear & o,p1,p3 is_collinear & o,q1,q2 is_collinear & o,q1,q3 is_collinear & p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear & p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear holds
r1,r2,r3 is_collinear ;
end;

:: deftheorem Def11 defines Fanoian ANPROJ_2:def 11 :
for IT being CollProjectiveSpace holds
( IT is Fanoian iff for p1, r2, q, r1, q1, p, r being Element of IT st p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear & r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear & not p1,r2,q1 is_collinear & not p1,r2,r1 is_collinear & not p1,r1,q1 is_collinear holds
r2,r1,q1 is_collinear );

:: deftheorem defines Desarguesian ANPROJ_2:def 12 :
for IT being CollProjectiveSpace holds
( IT is Desarguesian iff for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of IT st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not o,p1,p2 is_collinear & not o,p1,p3 is_collinear & not o,p2,p3 is_collinear & p1,p2,r3 is_collinear & q1,q2,r3 is_collinear & p2,p3,r1 is_collinear & q2,q3,r1 is_collinear & p1,p3,r2 is_collinear & q1,q3,r2 is_collinear & o,p1,q1 is_collinear & o,p2,q2 is_collinear & o,p3,q3 is_collinear holds
r1,r2,r3 is_collinear );

:: deftheorem defines Pappian ANPROJ_2:def 13 :
for IT being CollProjectiveSpace holds
( IT is Pappian iff for o, p1, p2, p3, q1, q2, q3, r1, r2, r3 being Element of IT st o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 is_collinear & o,p1,p2 is_collinear & o,p1,p3 is_collinear & o,q1,q2 is_collinear & o,q1,q3 is_collinear & p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear & p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear holds
r1,r2,r3 is_collinear );

definition
let IT be CollProjectiveSpace;
attr IT is 2-dimensional means :Def14: :: ANPROJ_2:def 14
for p, p1, q, q1 being Element of IT ex r being Element of IT st
( p,p1,r is_collinear & q,q1,r is_collinear );
end;

:: deftheorem Def14 defines 2-dimensional ANPROJ_2:def 14 :
for IT being CollProjectiveSpace holds
( IT is 2-dimensional iff for p, p1, q, q1 being Element of IT ex r being Element of IT st
( p,p1,r is_collinear & q,q1,r is_collinear ) );

notation
let IT be CollProjectiveSpace;
antonym up-3-dimensional IT for 2-dimensional IT;
end;

definition
let IT be CollProjectiveSpace;
attr IT is at_most-3-dimensional means :Def15: :: ANPROJ_2:def 15
for p, p1, q, q1, r2 being Element of IT ex r, r1 being Element of IT st
( p,q,r is_collinear & p1,q1,r1 is_collinear & r2,r,r1 is_collinear );
end;

:: deftheorem Def15 defines at_most-3-dimensional ANPROJ_2:def 15 :
for IT being CollProjectiveSpace holds
( IT is at_most-3-dimensional iff for p, p1, q, q1, r2 being Element of IT ex r, r1 being Element of IT st
( p,q,r is_collinear & p1,q1,r1 is_collinear & r2,r,r1 is_collinear ) );

theorem :: ANPROJ_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th28: :: ANPROJ_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non trivial RealLinearSpace
for p1, r2, q, r1, q1, p, r being Element of (ProjectiveSpace V) st p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear & r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear & not p1,r2,q1 is_collinear & not p1,r2,r1 is_collinear & not p1,r1,q1 is_collinear holds
r2,r1,q1 is_collinear
proof end;

Lm40: for V being up-3-dimensional RealLinearSpace holds ProjectiveSpace V is Fanoian
proof end;

Lm41: for V being up-3-dimensional RealLinearSpace holds ProjectiveSpace V is Desarguesian
proof end;

Lm42: for V being up-3-dimensional RealLinearSpace holds ProjectiveSpace V is Pappian
proof end;

registration
let V be up-3-dimensional RealLinearSpace;
cluster ProjectiveSpace V -> reflexive transitive proper Vebleian at_least_3rank Fanoian Desarguesian Pappian ;
coherence
( ProjectiveSpace V is Fanoian & ProjectiveSpace V is Desarguesian & ProjectiveSpace V is Pappian ) by Lm40, Lm41, Lm42;
end;

theorem Th29: :: ANPROJ_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non trivial RealLinearSpace st ex u, v, w being Element of V st
( ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) ) holds
ex x1, x2 being Element of (ProjectiveSpace V) st
( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st
( x1,x2,q is_collinear & r1,r2,q is_collinear ) ) )
proof end;

theorem Th30: :: ANPROJ_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non trivial RealLinearSpace st ex x1, x2 being Element of (ProjectiveSpace V) st
( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st
( x1,x2,q is_collinear & r1,r2,q is_collinear ) ) ) holds
for p, p1, q, q1 being Element of (ProjectiveSpace V) ex r being Element of (ProjectiveSpace V) st
( p,p1,r is_collinear & q,q1,r is_collinear )
proof end;

theorem Th31: :: ANPROJ_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non trivial RealLinearSpace st ex u, v, w being Element of V st
( ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) ) holds
ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is 2-dimensional )
proof end;

Lm43: for V being non trivial RealLinearSpace st ex y, u, v, w being Element of V st
for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) holds
V is up-3-dimensional
proof end;

Lm44: for V being non trivial RealLinearSpace st ex y, u, v, w being Element of V st
for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) holds
( ProjectiveSpace V is proper & ProjectiveSpace V is at_least_3rank )
proof end;

theorem Th32: :: ANPROJ_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non trivial RealLinearSpace st ex y, u, v, w being Element of V st
( ( for w1 being Element of V ex a, b, a1, b1 being Real st w1 = (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) ) & ( for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) ) holds
ex p, q1, q2 being Element of (ProjectiveSpace V) st
( not p,q1,q2 is_collinear & ( for r1, r2 being Element of (ProjectiveSpace V) ex q3, r3 being Element of (ProjectiveSpace V) st
( r1,r2,r3 is_collinear & q1,q2,q3 is_collinear & p,r3,q3 is_collinear ) ) )
proof end;

Lm45: for V being non trivial RealLinearSpace
for x, d, b, b', d', q being Element of (ProjectiveSpace V) st not q,b,d is_collinear & b,d,x is_collinear & q,b',b is_collinear & q,d',d is_collinear holds
ex o being Element of (ProjectiveSpace V) st
( b',d',o is_collinear & q,x,o is_collinear )
proof end;

theorem Th33: :: ANPROJ_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non trivial RealLinearSpace st ProjectiveSpace V is proper & ProjectiveSpace V is at_least_3rank & ex p, q1, q2 being Element of (ProjectiveSpace V) st
( not p,q1,q2 is_collinear & ( for r1, r2 being Element of (ProjectiveSpace V) ex q3, r3 being Element of (ProjectiveSpace V) st
( r1,r2,r3 is_collinear & q1,q2,q3 is_collinear & p,r3,q3 is_collinear ) ) ) holds
ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is at_most-3-dimensional )
proof end;

theorem Th34: :: ANPROJ_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non trivial RealLinearSpace st ex y, u, v, w being Element of V st
( ( for w1 being Element of V ex a, b, c, c1 being Real st w1 = (((a * y) + (b * u)) + (c * v)) + (c1 * w) ) & ( for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) ) holds
ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is at_most-3-dimensional )
proof end;

theorem Th35: :: ANPROJ_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non trivial RealLinearSpace st ex u, v, u1, v1 being Element of V st
for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) holds
ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & not CS is 2-dimensional )
proof end;

theorem Th36: :: ANPROJ_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being non trivial RealLinearSpace st ex u, v, u1, v1 being Element of V st
( ( for w being Element of V ex a, b, a1, b1 being Real st w = (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) ) & ( for a, b, a1, b1 being Real st (((a * u) + (b * v)) + (a1 * u1)) + (b1 * v1) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ) ) holds
ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & not CS is 2-dimensional & CS is at_most-3-dimensional )
proof end;

registration
cluster strict Fanoian Desarguesian Pappian 2-dimensional CollStr ;
existence
ex b1 being CollProjectiveSpace st
( b1 is strict & b1 is Fanoian & b1 is Desarguesian & b1 is Pappian & b1 is 2-dimensional )
proof end;
cluster strict Fanoian Desarguesian Pappian up-3-dimensional at_most-3-dimensional CollStr ;
existence
ex b1 being CollProjectiveSpace st
( b1 is strict & b1 is Fanoian & b1 is Desarguesian & b1 is Pappian & b1 is at_most-3-dimensional & not b1 is 2-dimensional )
proof end;
end;

definition
mode CollProjectivePlane is 2-dimensional CollProjectiveSpace;
end;

theorem :: ANPROJ_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CS being non empty CollStr holds
( CS is 2-dimensional CollProjectiveSpace iff ( CS is proper at_least_3rank CollSp & ( for p, p1, q, q1 being Element of CS ex r being Element of CS st
( p,p1,r is_collinear & q,q1,r is_collinear ) ) ) )
proof end;