defpred S₁[ object , object ] means ex B, C being Subset of (Prop Q) 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 (Class (PropRel Q)),(Class (PropRel Q)) such that
A1: for x, y being object 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 (Prop Q) 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 (Prop Q); :: 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 B9, C9 being Subset of (Prop Q) st
( B = B9 & C = C9 & ( for p, q being Element of Prop Q st p in B9 & q in C9 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 (Class (PropRel Q)) st
for B, C being Subset of (Prop Q) 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