let CPS be proper CollSp; :: thesis: for x being set holds
( x is LINE of CPS iff x is Element of ProjectiveLines CPS )
let x be set ; :: thesis: ( x is LINE of CPS iff x is Element of ProjectiveLines CPS )
hereby :: thesis: ( x is Element of ProjectiveLines CPS implies x is LINE of CPS )
assume x is LINE of CPS ; :: thesis: x is Element of ProjectiveLines CPS
then x in { B where B is Subset of CPS : B is LINE of CPS } ;
hence x is Element of ProjectiveLines CPS ; :: thesis: verum
end;
assume x is Element of ProjectiveLines CPS ; :: thesis: x is LINE of CPS
then x in ProjectiveLines CPS ;
then ex B being Subset of CPS st
( x = B & B is LINE of CPS ) ;
hence x is LINE of CPS ; :: thesis: verum