take id L ; :: thesis: ( id L is sups-preserving & id L is infs-preserving & id L is closure & id L is kernel & id L is V7() )
thus ( id L is sups-preserving & id L is infs-preserving & id L is closure & id L is kernel & id L is V7() ) ; :: thesis: verum