let n be Element of NAT ; :: thesis: for x1, x2, x3 being Element of REAL n holds
( Line x1,x2 c= plane x1,x2,x3 & Line x2,x3 c= plane x1,x2,x3 & Line x3,x1 c= plane x1,x2,x3 )
let x1, x2, x3 be Element of REAL n; :: thesis: ( Line x1,x2 c= plane x1,x2,x3 & Line x2,x3 c= plane x1,x2,x3 & Line x3,x1 c= plane x1,x2,x3 )
A1: x3 in plane x1,x2,x3 by Th87;
( x1 in plane x1,x2,x3 & x2 in plane x1,x2,x3 ) by Th87;
hence ( Line x1,x2 c= plane x1,x2,x3 & Line x2,x3 c= plane x1,x2,x3 & Line x3,x1 c= plane x1,x2,x3 ) by A1, Th90; :: thesis: verum