defpred S₁[ set , set ] means ex B, C being Subset of st
( $1 = B & $2 = C & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) );
consider R being Relation of , such that
A1: for x, y being set holds
( [x,y] in R iff ( x in Class (PropRel Q) & y in Class (PropRel Q) & S₁[x,y] ) ) from RELSET_1:sch 1();
for B, C being Subset of holds
( [B,C] in R iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) )

proof

let B, C be Subset of ; :: thesis: ( [B,C] in R iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) )
thus ( [B,C] in R implies ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) :: thesis: ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) implies [B,C] in R )

proof

assume A2: [B,C] in R ; :: thesis: ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) )
then ex B', C' being Subset of st
( B = B' & C = C' & ( for p, q being Element of Prop Q st p in B' & q in C' holds
p |- q ) ) by A1;
hence ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) by A1, A2; :: thesis: verum

end;

assume ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ; :: thesis: [B,C] in R
hence [B,C] in R by A1; :: thesis: verum

end;

hence ex b₁ being Relation of st
for B, C being Subset of holds
( [B,C] in b₁ iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ; :: thesis: verum