defpred S₁[ object ] means ex C being strict MSSubAlgebra of A st
( $1 = C & B is MSSubAlgebra of C );
consider IT being set such that
A1: for x being object holds
( x in IT iff ( x in MSSub A & S₁[x] ) ) from XBOOLE_0:sch 1();
take IT ; :: thesis: for x being object holds
( x in IT iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) )
let x be object ; :: thesis: ( x in IT iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) )
thus ( x in IT implies ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) ) by A1; :: thesis: ( ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) implies x in IT )
given C being strict MSSubAlgebra of A such that A2: x = C and
A3: B is MSSubAlgebra of C ; :: thesis: x in IT
x in MSSub A by A2, MSUALG_2:def 19;
hence x in IT by A1, A2, A3; :: thesis: verum