defpred S₁[ object , object ] means ex A, X being Subset of AS st
( $1 = LDir A & $2 = PDir X & A is being_line & X is being_plane & A '||' X );
set VV1 = Dir_of_Lines AS;
set VV2 = Dir_of_Planes AS;
consider P being Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) such that
A1: for x, y being object holds
( [x,y] in P iff ( x in Dir_of_Lines AS & y in Dir_of_Planes AS & S₁[x,y] ) ) from RELSET_1:sch 1();
take P ; :: 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 ) )
let x, y be object ; :: thesis: ( [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 ) )
thus ( [x,y] in P implies 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 A1; :: thesis: ( 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 [x,y] in P )
assume A2: 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: [x,y] in P
then A3: y in Dir_of_Planes AS by Th15;
x in Dir_of_Lines AS by A2, Th14;
hence [x,y] in P by A1, A2, A3; :: thesis: verum