let V be RealLinearSpace; :: thesis: for u, v, w being Element of V st not u,v,w are_LinDep holds
( not u is zero & not v is zero & not w is zero & not are_Prop u,v & not are_Prop v,w & not are_Prop w,u )
let u, v, w be Element of V; :: thesis: ( not u,v,w are_LinDep implies ( not u is zero & not v is zero & not w is zero & not are_Prop u,v & not are_Prop v,w & not are_Prop w,u ) )
assume A1: not u,v,w are_LinDep ; :: thesis: ( not u is zero & not v is zero & not w is zero & not are_Prop u,v & not are_Prop v,w & not are_Prop w,u )
then A2: w <> 0. V by Th15;
( u <> 0. V & v <> 0. V ) by A1, Th15;
hence ( not u is zero & not v is zero & not w is zero ) by A2, STRUCT_0:def 12; :: thesis: ( not are_Prop u,v & not are_Prop v,w & not are_Prop w,u )
thus ( not are_Prop u,v & not are_Prop v,w & not are_Prop w,u ) by A1, Th16; :: thesis: verum