let AS be AffinSpace; for a, b being Element of AS
for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & b in X & a in Y & b in Y & X <> Y & a <> b holds
X /\ Y is being_line
let a, b be Element of AS; for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & b in X & a in Y & b in Y & X <> Y & a <> b holds
X /\ Y is being_line
let X, Y be Subset of AS; ( X is being_plane & Y is being_plane & a in X & b in X & a in Y & b in Y & X <> Y & a <> b implies X /\ Y is being_line )
assume that
A1:
X is being_plane
and
A2:
Y is being_plane
and
A3:
( a in X & b in X )
and
A4:
( a in Y & b in Y )
and
A5:
X <> Y
and
A6:
a <> b
; X /\ Y is being_line
set Z = X /\ Y;
set Q = Line (a,b);
A7:
Line (a,b) c= X
by A1, A3, A6, Th19;
A8:
Line (a,b) c= Y
by A2, A4, A6, Th19;
A9:
Line (a,b) is being_line
by A6, AFF_1:def 3;
A10:
X /\ Y c= Line (a,b)
proof
assume
not
X /\ Y c= Line (
a,
b)
;
contradiction
then consider x being
object such that A11:
x in X /\ Y
and A12:
not
x in Line (
a,
b)
;
reconsider a9 =
x as
Element of
AS by A11;
A13:
x in Y
by A11, XBOOLE_0:def 4;
A14:
x in X
by A11, XBOOLE_0:def 4;
for
y being
object holds
(
y in X iff
y in Y )
proof
let y be
object ;
( y in X iff y in Y )
A15:
now ( y in Y implies y in X )assume A16:
y in Y
;
y in Xnow ( y <> x implies y in X )reconsider b9 =
y as
Element of
AS by A16;
set M =
Line (
a9,
b9);
A17:
a9 in Line (
a9,
b9)
by AFF_1:15;
A18:
b9 in Line (
a9,
b9)
by AFF_1:15;
assume A19:
y <> x
;
y in Xthen A20:
Line (
a9,
b9) is
being_line
by AFF_1:def 3;
A21:
Line (
a9,
b9)
c= Y
by A2, A13, A16, A19, Th19;
A22:
now ( not Line (a9,b9) // Line (a,b) implies y in X )assume
not
Line (
a9,
b9)
// Line (
a,
b)
;
y in Xthen consider q being
Element of
AS such that A23:
q in Line (
a9,
b9)
and A24:
q in Line (
a,
b)
by A2, A9, A8, A20, A21, Th22;
Line (
a9,
b9)
= Line (
a9,
q)
by A12, A20, A17, A23, A24, AFF_1:57;
then
Line (
a9,
b9)
c= X
by A1, A7, A12, A14, A24, Th19;
hence
y in X
by A18;
verum end; hence
y in X
by A22;
verum end; hence
y in X
by A11, XBOOLE_0:def 4;
verum end;
now ( y in X implies y in Y )assume A25:
y in X
;
y in Ynow ( y <> x implies y in Y )reconsider b9 =
y as
Element of
AS by A25;
set M =
Line (
a9,
b9);
A26:
a9 in Line (
a9,
b9)
by AFF_1:15;
A27:
b9 in Line (
a9,
b9)
by AFF_1:15;
assume A28:
y <> x
;
y in Ythen A29:
Line (
a9,
b9) is
being_line
by AFF_1:def 3;
A30:
Line (
a9,
b9)
c= X
by A1, A14, A25, A28, Th19;
A31:
now ( not Line (a9,b9) // Line (a,b) implies y in Y )assume
not
Line (
a9,
b9)
// Line (
a,
b)
;
y in Ythen consider q being
Element of
AS such that A32:
q in Line (
a9,
b9)
and A33:
q in Line (
a,
b)
by A1, A9, A7, A29, A30, Th22;
Line (
a9,
b9)
= Line (
a9,
q)
by A12, A29, A26, A32, A33, AFF_1:57;
then
Line (
a9,
b9)
c= Y
by A2, A8, A12, A13, A33, Th19;
hence
y in Y
by A27;
verum end; hence
y in Y
by A31;
verum end; hence
y in Y
by A11, XBOOLE_0:def 4;
verum end;
hence
(
y in X iff
y in Y )
by A15;
verum
end;
hence
contradiction
by A5, TARSKI:2;
verum
end;
Line (a,b) c= X /\ Y
by A7, A8, XBOOLE_1:19;
hence
X /\ Y is being_line
by A9, A10, XBOOLE_0:def 10; verum