defpred S1[ FormalConcept of C, FormalConcept of C, set ] means ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( $3 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of $1 \/ the Extent of $2)) & A = the Intent of $1 /\ the Intent of $2 );
A1:
for CP1, CP2 being Element of B-carrier C ex CP being Element of B-carrier C st S1[CP1,CP2,CP]
proof
let CP1,
CP2 be
Element of
B-carrier C;
ex CP being Element of B-carrier C st S1[CP1,CP2,CP]
set O =
(AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2));
set A = the
Intent of
CP1 /\ the
Intent of
CP2;
reconsider O9 = the
Extent of
CP1 \/ the
Extent of
CP2 as
Subset of the
carrier of
C ;
set CP =
ConceptStr(#
((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))),
( the Intent of CP1 /\ the Intent of CP2) #);
A2:
(ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))) =
(ObjectDerivation C) . O9
by Th7
.=
((ObjectDerivation C) . the Extent of CP1) /\ ((ObjectDerivation C) . the Extent of CP2)
by Th15
.=
the
Intent of
CP1 /\ ((ObjectDerivation C) . the Extent of CP2)
by Def9
.=
the
Intent of
CP1 /\ the
Intent of
CP2
by Def9
;
then
(
(AttributeDerivation C) . ( the Intent of CP1 /\ the Intent of CP2) = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) & not
ConceptStr(#
((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))),
( the Intent of CP1 /\ the Intent of CP2) #) is
empty )
by Lm1, Th7;
then
ConceptStr(#
((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))),
( the Intent of CP1 /\ the Intent of CP2) #)
in { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) }
by A2;
hence
ex
CP being
Element of
B-carrier C st
S1[
CP1,
CP2,
CP]
;
verum
end;
consider f being Function of [:(B-carrier C),(B-carrier C):],(B-carrier C) such that
A3:
for CP1, CP2 being Element of B-carrier C holds S1[CP1,CP2,f . (CP1,CP2)]
from BINOP_1:sch 3(A1);
reconsider f = f as BinOp of (B-carrier C) ;
take
f
; for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . (CP1,CP2) = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) & A = the Intent of CP1 /\ the Intent of CP2 )
for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . (CP1,CP2) = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) & A = the Intent of CP1 /\ the Intent of CP2 )
hence
for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . (CP1,CP2) = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) & A = the Intent of CP1 /\ the Intent of CP2 )
; verum