defpred S1[ object , object ] means ( ex K being Subset of AS st
( K is being_line & $2 = [K,1] & ( ( $1 in the carrier of AS & $1 in K ) or $1 = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & $1 = LDir K & $2 = [(PDir X),2] & K '||' X ) );
set VV1 = ProjectivePoints AS;
set VV2 = ProjectiveLines AS;
consider P being Relation of (ProjectivePoints AS),(ProjectiveLines AS) such that
A1: for x, y being object holds
( [x,y] in P iff ( x in ProjectivePoints AS & y in ProjectiveLines AS & S1[x,y] ) ) from RELSET_1:sch 1();
 take P ; :: thesis: for x, y being object holds
( [x,y] in P iff ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) )
let x, y be object ; :: thesis: ( [x,y] in P iff ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) )
thus ( not [x,y] in P or ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) by A1; :: thesis: ( ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) implies [x,y] in P )
assume A2: ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ; :: thesis: [x,y] in P
( x in ProjectivePoints AS & y in ProjectiveLines AS )
proof
A3: now :: thesis: ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) implies ( x in ProjectivePoints AS & y in ProjectiveLines AS ) )
given K being Subset of AS such that A4: K is being_line and
A5: y = [K,1] and
A6: ( ( x in the carrier of AS & x in K ) or x = LDir K ) ; :: thesis: ( x in ProjectivePoints AS & y in ProjectiveLines AS )
y in [:(AfLines AS),{1}:] by A4, A5, Th18;
hence ( x in ProjectivePoints AS & y in ProjectiveLines AS ) by A6, A7, XBOOLE_0:def 3; :: thesis: verum
end;
now :: thesis: ( ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) implies ( x in ProjectivePoints AS & y in ProjectiveLines AS ) )
given K, X being Subset of AS such that A8: K is being_line and
A9: X is being_plane and
A10: x = LDir K and
A11: y = [(PDir X),2] and
K '||' X ; :: thesis: ( x in ProjectivePoints AS & y in ProjectiveLines AS )
x in Dir_of_Lines AS by A8, A10, Th14;
hence x in ProjectivePoints AS by XBOOLE_0:def 3; :: thesis: y in ProjectiveLines AS
y in [:(Dir_of_Planes AS),{2}:] by A9, A11, Th19;
hence y in ProjectiveLines AS by XBOOLE_0:def 3; :: thesis: verum
end;
hence ( x in ProjectivePoints AS & y in ProjectiveLines AS ) by A2, A3; :: thesis: verum
end;
hence [x,y] in P by A1, A2; :: thesis: verum