let OO, Ox, Oy be Element of REAL 2; ( OO = |[0,0]| & Ox = |[1,0]| & Oy = |[0,1]| implies REAL 2 = plane (OO,Ox,Oy) )
assume that
A1:
OO = |[0,0]|
and
A2:
Ox = |[1,0]|
and
A3:
Oy = |[0,1]|
; REAL 2 = plane (OO,Ox,Oy)
now for a being object st a in REAL 2 holds
a in plane (OO,Ox,Oy)let a be
object ;
( a in REAL 2 implies a in plane (OO,Ox,Oy) )assume
a in REAL 2
;
a in plane (OO,Ox,Oy)then reconsider b =
a as
Point of
(TOP-REAL 2) by EUCLID:22;
A4:
b =
|[((b `1) + 0),(0 + (b `2))]|
by EUCLID:53
.=
|[((b `1) * 1),((b `1) * 0)]| + |[((b `2) * 0),((b `2) * 1)]|
by EUCLID:56
.=
((b `1) * |[1,0]|) + |[((b `2) * 0),((b `2) * 1)]|
by EUCLID:58
.=
((b `1) * |[1,0]|) + ((b `2) * |[0,1]|)
by EUCLID:58
;
reconsider a1 = 1
- ((b `1) + (b `2)) as
Real ;
reconsider a2 =
b `1 as
Real ;
reconsider a3 =
b `2 as
Real ;
a1 * |[0,0]| =
|[(a1 * 0),(a1 * 0)]|
by EUCLID:58
.=
|[0,0]|
;
then (a1 * |[0,0]|) + b =
|[0,0]| + |[(b `1),(b `2)]|
by EUCLID:53
.=
|[(0 + (b `1)),(0 + (b `2))]|
by EUCLID:56
.=
b
by EUCLID:53
;
then A5:
b = ((a1 * |[0,0]|) + (a2 * |[1,0]|)) + (a3 * |[0,1]|)
by A4, RLVECT_1:def 3;
(
(a1 + a2) + a3 = 1 &
b = ((a1 * OO) + (a2 * Ox)) + (a3 * Oy) )
by A1, A2, A5, A3;
then
a in { x where x is Element of REAL 2 : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & x = ((a1 * OO) + (a2 * Ox)) + (a3 * Oy) ) }
;
hence
a in plane (
OO,
Ox,
Oy)
by EUCLIDLP:def 9;
verum end;
then
REAL 2 c= plane (OO,Ox,Oy)
;
hence
REAL 2 = plane (OO,Ox,Oy)
; verum