let C be FormalContext; :: thesis: ( rng (gamma C) is supremum-dense & rng (delta C) is infimum-dense )
set G = rng (gamma C);
thus rng (gamma C) is supremum-dense :: thesis: rng (delta C) is infimum-dense

proof

let a be Element of ; :: according to LATTICE6:def 13 :: thesis: ex b₁ being Element of bool (rng (gamma C)) st a = "\/" b₁,(ConceptLattice C)
A1: { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex o being Object of st
( o in the Extent of (a @ ) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } c= rng (gamma C)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex o being Object of st
( o in the Extent of (a @ ) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } or x in rng (gamma C) )
assume x in { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex o being Object of st
( o in the Extent of (a @ ) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } ; :: thesis: x in rng (gamma C)
then consider O being Subset of , A being Subset of such that
A2: x = ConceptStr(# O,A #) and
A3: ex o being Object of st
( o in the Extent of (a @ ) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ;
consider o being Object of such that
o in the Extent of (a @ ) and
O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) and
A4: A = (ObjectDerivation C) . {o} by A3;
consider y being Element of such that
A5: (gamma C) . o = y ;
( dom (gamma C) = the carrier of C & ex O' being Subset of ex A' being Subset of st
( y = ConceptStr(# O',A' #) & O' = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A' = (ObjectDerivation C) . {o} ) ) by A5, Def4, FUNCT_2:def 1;
hence x in rng (gamma C) by A2, A3, A4, A5, FUNCT_1:def 5; :: thesis: verum

end;

( "\/" { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex o being Object of st
( o in the Extent of (a @ ) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } ,(ConceptLattice C) = a @ & a = a @ ) by Th9, CONLAT_1:def 24;
hence ex b₁ being Element of bool (rng (gamma C)) st a = "\/" b₁,(ConceptLattice C) by A1; :: thesis: verum

end;

let b be Element of ; :: according to LATTICE6:def 14 :: thesis: ex b₁ being Element of bool (rng (delta C)) st b = "/\" b₁,(ConceptLattice C)
set G = rng (delta C);
A6: { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex a being Attribute of st
( a in the Intent of (b @ ) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } c= rng (delta C)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex a being Attribute of st
( a in the Intent of (b @ ) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } or x in rng (delta C) )
assume x in { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex a being Attribute of st
( a in the Intent of (b @ ) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ; :: thesis: x in rng (delta C)
then consider O being Subset of , A being Subset of such that
A7: x = ConceptStr(# O,A #) and
A8: ex a being Attribute of st
( a in the Intent of (b @ ) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ;
consider a being Attribute of such that
a in the Intent of (b @ ) and
A9: O = (AttributeDerivation C) . {a} and
A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) by A8;
consider y being Element of such that
A10: (delta C) . a = y ;
( dom (delta C) = the carrier' of C & ex O' being Subset of ex A' being Subset of st
( y = ConceptStr(# O',A' #) & O' = (AttributeDerivation C) . {a} & A' = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) by A10, Def5, FUNCT_2:def 1;
hence x in rng (delta C) by A7, A8, A9, A10, FUNCT_1:def 5; :: thesis: verum

end;

( "/\" { ConceptStr(# O,A #) where O is Subset of , A is Subset of : ex a being Attribute of st
( a in the Intent of (b @ ) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ,(ConceptLattice C) = b @ & b = b @ ) by Th10, CONLAT_1:def 24;
hence ex b₁ being Element of bool (rng (delta C)) st b = "/\" b₁,(ConceptLattice C) by A6; :: thesis: verum