let POS be OrtAfSp; :: thesis: for X being Subset of POS
for Y being Subset of (Af 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 (Af POS) st X = Y holds
( X is being_line iff Y is being_line )
let Y be Subset of (Af 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 & X = Line a,b ) by Def13;
reconsider a' = a, b' = b as Element of (Af POS) ;
Y = Line a',b' by A1, A2, Th56;
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 a', b' being Element of (Af POS) such that
A3: ( a' <> b' & Y = Line a',b' ) by AFF_1:def 3;
reconsider a = a', b = b' as Element of POS ;
X = Line a,b by A1, A3, Th56;
hence X is being_line by A3, Def13; :: thesis: verum