let AS be AffinSpace; :: thesis: for a, b being Element of AS

for X being Subset of AS st X is being_plane & a in X & b in X & a <> b holds

Line (a,b) c= X

let a, b be Element of AS; :: thesis: for X being Subset of AS st X is being_plane & a in X & b in X & a <> b holds

Line (a,b) c= X

let X be Subset of AS; :: thesis: ( X is being_plane & a in X & b in X & a <> b implies Line (a,b) c= X )

assume that

A1: X is being_plane and

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

A3: a <> b ; :: thesis: Line (a,b) c= X

set Q = Line (a,b);

A4: ( a in Line (a,b) & b in Line (a,b) ) by AFF_1:15;

( Line (a,b) is being_line & ex K, P being Subset of AS st

( K is being_line & P is being_line & not K // P & X = Plane (K,P) ) ) by A1, A3, AFF_1:def 3;

hence Line (a,b) c= X by A2, A3, A4, Lm5; :: thesis: verum

for X being Subset of AS st X is being_plane & a in X & b in X & a <> b holds

Line (a,b) c= X

let a, b be Element of AS; :: thesis: for X being Subset of AS st X is being_plane & a in X & b in X & a <> b holds

Line (a,b) c= X

let X be Subset of AS; :: thesis: ( X is being_plane & a in X & b in X & a <> b implies Line (a,b) c= X )

assume that

A1: X is being_plane and

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

A3: a <> b ; :: thesis: Line (a,b) c= X

set Q = Line (a,b);

A4: ( a in Line (a,b) & b in Line (a,b) ) by AFF_1:15;

( Line (a,b) is being_line & ex K, P being Subset of AS st

( K is being_line & P is being_line & not K // P & X = Plane (K,P) ) ) by A1, A3, AFF_1:def 3;

hence Line (a,b) c= X by A2, A3, A4, Lm5; :: thesis: verum