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