defpred S₁[ set ] means ex a being Element of Q. I st $1 = QClass. a;
let F1, F2 be Subset-Family of (Q. I); :: thesis: ( ( for A being Subset of (Q. I) holds
( A in F1 iff ex u being Element of Q. I st A = QClass. u ) ) & ( for A being Subset of (Q. I) holds
( A in F2 iff ex u being Element of Q. I st A = QClass. u ) ) implies F1 = F2 )
assume A1: for A being Subset of (Q. I) holds
( A in F1 iff S₁[A] ) ; :: thesis: ( ex A being Subset of (Q. I) st
( ( A in F2 implies ex u being Element of Q. I st A = QClass. u ) implies ( ex u being Element of Q. I st A = QClass. u & not A in F2 ) ) or F1 = F2 )
assume A2: for A being Subset of (Q. I) holds
( A in F2 iff S₁[A] ) ; :: thesis: F1 = F2
thus F1 = F2 from SUBSET_1:sch 4(A1, A2); :: thesis: verum