let P, Q be Relation of (ProjectivePoints AS),(ProjectiveLines AS); :: 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 ) ) ) ) & ( for x, y being object holds
( [x,y] in Q 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 ) ) ) ) implies P = Q )
assume that
A12: 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 ) ) ) and
A13: for x, y being object holds
( [x,y] in Q 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 ) ) ) ; :: thesis: P = Q
for x, y being object holds
( [x,y] in P iff [x,y] in Q )
proof
let x, y be object ; :: thesis: ( [x,y] in P iff [x,y] in Q )
( [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 ) ) ) by A12;
hence ( [x,y] in P iff [x,y] in Q ) by A13; :: thesis: verum
end;
hence P = Q by RELAT_1:def 2; :: thesis: verum