let AS be AffinSpace; :: thesis: for x being set holds
( x in [:(AfLines AS),{1}:] iff ex X being Subset of AS st
( x = [X,1] & X is being_line ) )
let x be set ; :: thesis: ( x in [:(AfLines AS),{1}:] iff ex X being Subset of AS st
( x = [X,1] & X is being_line ) )
A1: now :: thesis: ( x in [:(AfLines AS),{1}:] implies ex X being Subset of AS st
( x = [X,1] & X is being_line ) )
assume x in [:(AfLines AS),{1}:] ; :: thesis: ex X being Subset of AS st
( x = [X,1] & X is being_line )
then consider x1, x2 being object such that
A2: x1 in AfLines AS and
A3: x2 in {1} and
A4: x = [x1,x2] by ZFMISC_1:def 2;
consider X being Subset of AS such that
A5: x1 = X and
A6: X is being_line by A2;
take X = X; :: thesis: ( x = [X,1] & X is being_line )
thus x = [X,1] by A3, A4, A5, TARSKI:def 1; :: thesis: X is being_line
thus X is being_line by A6; :: thesis: verum
end;
now :: thesis: ( ex X being Subset of AS st
( x = [X,1] & X is being_line ) implies x in [:(AfLines AS),{1}:] )
given X being Subset of AS such that A7: x = [X,1] and
A8: X is being_line ; :: thesis: x in [:(AfLines AS),{1}:]
X in AfLines AS by A8;
hence x in [:(AfLines AS),{1}:] by A7, ZFMISC_1:106; :: thesis: verum
end;
hence ( x in [:(AfLines AS),{1}:] iff ex X being Subset of AS st
( x = [X,1] & X is being_line ) ) by A1; :: thesis: verum