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; :: thesis: 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; :: according to XBOOLE_0:def 10,AOFA_A00:def 31 :: thesis: ( 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 b₁, b₂ being object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*b₁*> = 'not' b₁ & (Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*b₁,b₂*> = b₁ '&' b₂ ) ) )
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; :: thesis: ( (Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {} = TRUE & ( for b₁, b₂ being object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*b₁*> = 'not' b₁ & (Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*b₁,b₂*> = b₁ '&' b₂ ) ) )
thus (Den ((In (( the connectives of S . 1), the carrier' of S)),B)) . {} = TRUE by A4; :: thesis: for b₁, b₂ being object holds
( (Den ((In (( the connectives of S . 2), the carrier' of S)),B)) . <*b₁*> = 'not' b₁ & (Den ((In (( the connectives of S . 3), the carrier' of S)),B)) . <*b₁,b₂*> = b₁ '&' b₂ )
let x, y be boolean object ; :: thesis: ( (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 ; :: thesis: (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 ;
:: thesis: verum