A1:
( the Sorts of A . the bool-sort of S = BOOLEAN & (Den ((In (( the connectives of S . 1), the carrier' of S)),A)) . {} = TRUE & ( for x, y being boolean object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),A)) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),A)) . <*x,y*> = x '&' y ) ) )
by AOFA_A00:def 32;
let B be non-empty MSSubAlgebra of A; B is bool-correct
the Sorts of B is MSSubset of A
by MSUALG_2:def 9;
hence
the Sorts of B . the bool-sort of S c= BOOLEAN
by A1, PBOOLE:def 18, PBOOLE:def 2; XBOOLE_0:def 10,AOFA_A00:def 31 ( BOOLEAN c= the Sorts of B . the bool-sort of S & (Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {} = TRUE & ( for b1, b2 being object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*b1*> = 'not' b1 & (Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*b1,b2*> = b1 '&' b2 ) ) )
set o1 = In (( the connectives of S . 1), the carrier' of S);
set o2 = In (( the connectives of S . 2), the carrier' of S);
set b = the bool-sort of S;
3 <= len the connectives of S
by AOFA_A00:def 31;
then
1 <= len the connectives of S
by XXREAL_0:2;
then
1 in dom the connectives of S
by FINSEQ_3:25;
then
In (( the connectives of S . 1), the carrier' of S) = the connectives of S . 1
by FUNCT_1:102, SUBSET_1:def 8;
then
In (( the connectives of S . 1), the carrier' of S) is_of_type {} , the bool-sort of S
by AOFA_A00:def 31;
then A2:
( Den ((In (( the connectives of S . 1), the carrier' of S)),B) is Function of (( the Sorts of B #) . {}),( the Sorts of B . the bool-sort of S) & Args ((In (( the connectives of S . 1), the carrier' of S)),B) = ( the Sorts of B #) . {} )
by Th7;
( the Sorts of B #) . (<*> the carrier of S) = {{}}
by PRE_CIRC:2;
then A3:
{} in ( the Sorts of B #) . {}
by TARSKI:def 1;
A4: (Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {} =
(Den ((In (( the connectives of S . 1), the carrier' of S)),A)) . {}
by A2, A3, EQUATION:19
.=
TRUE
by AOFA_A00:def 32
;
then A5:
TRUE in the Sorts of B . the bool-sort of S
by A2, A3, FUNCT_2:5;
A6:
<* the bool-sort of S*> in the carrier of S *
by FINSEQ_1:def 11;
A7:
dom the Sorts of B = the carrier of S
by PARTFUN1:def 2;
3 <= len the connectives of S
by AOFA_A00:def 31;
then
2 <= len the connectives of S
by XXREAL_0:2;
then
2 in dom the connectives of S
by FINSEQ_3:25;
then
In (( the connectives of S . 2), the carrier' of S) = the connectives of S . 2
by FUNCT_1:102, SUBSET_1:def 8;
then
In (( the connectives of S . 2), the carrier' of S) is_of_type <* the bool-sort of S*>, the bool-sort of S
by AOFA_A00:def 31;
then A8:
( Den ((In (( the connectives of S . 2), the carrier' of S)),B) is Function of (( the Sorts of B #) . <* the bool-sort of S*>),( the Sorts of B . the bool-sort of S) & Args ((In (( the connectives of S . 2), the carrier' of S)),B) = ( the Sorts of B #) . <* the bool-sort of S*> )
by Th7;
then A9: Args ((In (( the connectives of S . 2), the carrier' of S)),B) =
product ( the Sorts of B * <* the bool-sort of S*>)
by A6, FINSEQ_2:def 5
.=
product <*( the Sorts of B . the bool-sort of S)*>
by A7, FINSEQ_2:34
;
then A10:
<*TRUE*> in Args ((In (( the connectives of S . 2), the carrier' of S)),B)
by A5, FINSEQ_3:123;
(Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*TRUE*> =
(Den ((In (( the connectives of S . 2), the carrier' of S)),A)) . <*TRUE*>
by A9, A5, FINSEQ_3:123, EQUATION:19
.=
'not' TRUE
by AOFA_A00:def 32
.=
FALSE
;
then
FALSE in the Sorts of B . the bool-sort of S
by A8, A10, FUNCT_2:5;
hence A11:
BOOLEAN c= the Sorts of B . the bool-sort of S
by A5, ZFMISC_1:32; ( (Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {} = TRUE & ( for b1, b2 being object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*b1*> = 'not' b1 & (Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*b1,b2*> = b1 '&' b2 ) ) )
thus
(Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {} = TRUE
by A4; for b1, b2 being object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*b1*> = 'not' b1 & (Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*b1,b2*> = b1 '&' b2 )
let x, y be boolean object ; ( (Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*x*> = 'not' x & (Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*x,y*> = x '&' y )
A12:
<* the bool-sort of S, the bool-sort of S*> in the carrier of S *
by FINSEQ_1:def 11;
A13:
( x in BOOLEAN & y in BOOLEAN )
by MARGREL1:def 12;
thus (Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*x*> =
(Den ((In (( the connectives of S . 2), the carrier' of S)),A)) . <*x*>
by A13, A11, A9, FINSEQ_3:123, EQUATION:19
.=
'not' x
by AOFA_A00:def 32
; (Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*x,y*> = x '&' y
set o3 = In (( the connectives of S . 3), the carrier' of S);
3 <= len the connectives of S
by AOFA_A00:def 31;
then
3 in dom the connectives of S
by FINSEQ_3:25;
then
In (( the connectives of S . 3), the carrier' of S) = the connectives of S . 3
by FUNCT_1:102, SUBSET_1:def 8;
then
In (( the connectives of S . 3), the carrier' of S) is_of_type <* the bool-sort of S, the bool-sort of S*>, the bool-sort of S
by AOFA_A00:def 31;
then
( Den ((In (( the connectives of S . 3), the carrier' of S)),B) is Function of (( the Sorts of B #) . <* the bool-sort of S, the bool-sort of S*>),( the Sorts of B . the bool-sort of S) & Args ((In (( the connectives of S . 3), the carrier' of S)),B) = ( the Sorts of B #) . <* the bool-sort of S, the bool-sort of S*> )
by Th7;
then Args ((In (( the connectives of S . 3), the carrier' of S)),B) =
product ( the Sorts of B * <* the bool-sort of S, the bool-sort of S*>)
by A12, FINSEQ_2:def 5
.=
product <*( the Sorts of B . the bool-sort of S),( the Sorts of B . the bool-sort of S)*>
by A7, FINSEQ_2:125
;
hence (Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*x,y*> =
(Den ((In (( the connectives of S . 3), the carrier' of S)),A)) . <*x,y*>
by A11, A13, FINSEQ_3:124, EQUATION:19
.=
x '&' y
by AOFA_A00:def 32
;
verum