let P, Q be Relation of (Dir_of_Lines AS),(Dir_of_Planes AS); :: thesis: ( ( for x, y being object holds
( [x,y] in P iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) ) & ( for x, y being object holds
( [x,y] in Q iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) ) implies P = Q )
assume that
A4: for x, y being object holds
( [x,y] in P iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) and
A5: for x, y being object holds
( [x,y] in Q iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' 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 A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) by A4;
hence ( [x,y] in P iff [x,y] in Q ) by A5; :: thesis: verum

end;

hence P = Q by RELAT_1:def 2; :: thesis: verum