let POS be OrtAfSp; :: thesis: for X being Subset of POS
for Y being Subset of AffinStruct(# the carrier of POS, the CONGR of POS #) st X = Y holds
( X is being_line iff Y is being_line )
let X be Subset of the carrier of POS; :: thesis: for Y being Subset of AffinStruct(# the carrier of POS, the CONGR of POS #) st X = Y holds
( X is being_line iff Y is being_line )
let Y be Subset of AffinStruct(# the carrier of POS, the CONGR of POS #); :: thesis: ( X = Y implies ( X is being_line iff Y is being_line ) )
assume A1: X = Y ; :: thesis: ( X is being_line iff Y is being_line )

hereby :: thesis: ( Y is being_line implies X is being_line )

assume X is being_line ; :: thesis: Y is being_line
then consider a, b being Element of POS such that
A2: a <> b and
A3: X = Line (a,b) ;
reconsider a9 = a, b9 = b as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
Y = Line (a9,b9) by A1, A3, Th41;
hence Y is being_line by A2, AFF_1:def 3; :: thesis: verum

end;

assume Y is being_line ; :: thesis: X is being_line
then consider a9, b9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) such that
A4: a9 <> b9 and
A5: Y = Line (a9,b9) by AFF_1:def 3;
reconsider a = a9, b = b9 as Element of POS ;
X = Line (a,b) by A1, A5, Th41;
hence X is being_line by A4; :: thesis: verum