let n be Nat; 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; ( 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 Th82;
( x1 in plane (x1,x2,x3) & x2 in plane (x1,x2,x3) )
by Th82;
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, Th85; verum