let AS be AffinSpace; :: thesis: for a, b, c 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 & c in X & a in Y & b in Y & c in Y & not LIN a,b,c holds

X = Y

let a, b, c be Element of AS; :: thesis: for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & b in X & c in X & a in Y & b in Y & c in Y & not LIN a,b,c holds

X = Y

let X, Y be Subset of AS; :: thesis: ( X is being_plane & Y is being_plane & a in X & b in X & c in X & a in Y & b in Y & c in Y & not LIN a,b,c implies X = Y )

assume that

A1: ( X is being_plane & Y is being_plane ) and

A2: ( a in X & b in X ) and

A3: c in X and

A4: ( a in Y & b in Y ) and

A5: c in Y and

A6: not LIN a,b,c ; :: thesis: X = Y

assume A7: not X = Y ; :: thesis: contradiction

a <> b by A6, AFF_1:7;

then A8: X /\ Y is being_line by A1, A2, A4, A7, Th24;

A9: c in X /\ Y by A3, A5, XBOOLE_0:def 4;

( a in X /\ Y & b in X /\ Y ) by A2, A4, XBOOLE_0:def 4;

hence contradiction by A6, A8, A9, AFF_1:21; :: thesis: verum

for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & b in X & c in X & a in Y & b in Y & c in Y & not LIN a,b,c holds

X = Y

let a, b, c be Element of AS; :: thesis: for X, Y being Subset of AS st X is being_plane & Y is being_plane & a in X & b in X & c in X & a in Y & b in Y & c in Y & not LIN a,b,c holds

X = Y

let X, Y be Subset of AS; :: thesis: ( X is being_plane & Y is being_plane & a in X & b in X & c in X & a in Y & b in Y & c in Y & not LIN a,b,c implies X = Y )

assume that

A1: ( X is being_plane & Y is being_plane ) and

A2: ( a in X & b in X ) and

A3: c in X and

A4: ( a in Y & b in Y ) and

A5: c in Y and

A6: not LIN a,b,c ; :: thesis: X = Y

assume A7: not X = Y ; :: thesis: contradiction

a <> b by A6, AFF_1:7;

then A8: X /\ Y is being_line by A1, A2, A4, A7, Th24;

A9: c in X /\ Y by A3, A5, XBOOLE_0:def 4;

( a in X /\ Y & b in X /\ Y ) by A2, A4, XBOOLE_0:def 4;

hence contradiction by A6, A8, A9, AFF_1:21; :: thesis: verum