defpred S1[ object , object ] means ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( $2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {$1}) & A = (ObjectDerivation C) . {$1} );
A1:
for e being object st e in the carrier of C holds
ex u being object st
( u in the carrier of (ConceptLattice C) & S1[e,u] )
proof
let e be
object ;
( e in the carrier of C implies ex u being object st
( u in the carrier of (ConceptLattice C) & S1[e,u] ) )
assume
e in the
carrier of
C
;
ex u being object st
( u in the carrier of (ConceptLattice C) & S1[e,u] )
then reconsider se =
{e} as
Subset of the
carrier of
C by ZFMISC_1:31;
set A =
(ObjectDerivation C) . se;
set O =
(AttributeDerivation C) . ((ObjectDerivation C) . se);
take
ConceptStr(#
((AttributeDerivation C) . ((ObjectDerivation C) . se)),
((ObjectDerivation C) . se) #)
;
( ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #) in the carrier of (ConceptLattice C) & S1[e, ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #)] )
(
ConceptLattice C = LattStr(#
(B-carrier C),
(B-join C),
(B-meet C) #) &
ConceptStr(#
((AttributeDerivation C) . ((ObjectDerivation C) . se)),
((ObjectDerivation C) . se) #) is
FormalConcept of
C )
by CONLAT_1:19, CONLAT_1:def 20;
hence
(
ConceptStr(#
((AttributeDerivation C) . ((ObjectDerivation C) . se)),
((ObjectDerivation C) . se) #)
in the
carrier of
(ConceptLattice C) &
S1[
e,
ConceptStr(#
((AttributeDerivation C) . ((ObjectDerivation C) . se)),
((ObjectDerivation C) . se) #)] )
by CONLAT_1:31;
verum
end;
consider f being Function of the carrier of C, the carrier of (ConceptLattice C) such that
A2:
for e being object st e in the carrier of C holds
S1[e,f . e]
from FUNCT_2:sch 1(A1);
take
f
; for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} )
let o be Element of C; ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} )
thus
ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} )
by A2; verum